X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?a=blobdiff_plain;ds=inline;f=week7.mdwn;h=84a2af55dec222f8d8e21eb9bb51c4ea38667508;hb=602a62cffb64edbfade4e04d94913fe0f571a7a9;hp=52bc8eb5d2e9855e872cfca13bc469d1582e8b36;hpb=f1086f391556371f688a6ed2807da5e127d69608;p=lambda.git diff --git a/week7.mdwn b/week7.mdwn index 52bc8eb5..84a2af55 100644 --- a/week7.mdwn +++ b/week7.mdwn @@ -5,10 +5,10 @@ Monads Start by (re)reading the discussion of monads in the lecture notes for week 6 [Towards Monads](http://lambda.jimpryor.net//week6/#index4h2). -In those notes, we saw a way to separate thining about error +In those notes, we saw a way to separate thinking about error conditions (such as trying to divide by zero) from thinking about normal arithmetic computations. We did this by making use of the -Option monad: in each place where we had something of type `int`, we +option monad: in each place where we had something of type `int`, we put instead something of type `int option`, which is a sum type consisting either of just an integer, or else some special value which we could interpret as signaling that something had gone wrong. @@ -16,19 +16,19 @@ we could interpret as signaling that something had gone wrong. The goal was to make normal computing as convenient as possible: when we're adding or multiplying, we don't have to worry about generating any new errors, so we do want to think about the difference between -ints and int options. We tried to accomplish this by defining a -`bind` operator, which enabled us to peel away the option husk to get +`int`s and `int option`s. We tried to accomplish this by defining a +`bind` operator, which enabled us to peel away the `option` husk to get at the delicious integer inside. There was also a homework problem -which made this even more convenient by mapping any bindary operation +which made this even more convenient by mapping any binary operation on plain integers into a lifted operation that understands how to deal -with int options in a sensible way. +with `int option`s in a sensible way. [Linguitics note: Dividing by zero is supposed to feel like a kind of presupposition failure. If we wanted to adapt this approach to building a simple account of presupposition projection, we would have to do several things. First, we would have to make use of the polymorphism of the `option` type. In the arithmetic example, we only -made use of int options, but when we're composing natural language +made use of `int option`s, but when we're composing natural language expression meanings, we'll need to use types like `N int`, `Det Int`, `VP int`, and so on. But that works automatically, because we can use any type for the `'a` in `'a option`. Ultimately, we'd want to have a @@ -38,7 +38,7 @@ material that otherwise would trigger a presupposition violation; but, not surprisingly, these refinements will require some more sophisticated techniques than the super-simple option monad.] -So what examctly is a monad? As usual, we're not going to be pedantic +So what exactly is a monad? As usual, we're not going to be pedantic about it, but for our purposes, we can consider a monad to be a system that provides at least the following three elements: @@ -51,7 +51,7 @@ that provides at least the following three elements: `type 'a option = None | Some of 'a;;` * A way to turn an ordinary value into a monadic value. In Ocaml, we - did this for any integer n by mapping an arbitrary integer `n` to + did this for any integer `n` by mapping it to the option `Some n`. To be official, we can define a function called unit: @@ -86,10 +86,19 @@ that provides at least the following three elements: happend to be a box containing an integer `n`, this allowed us to get our hands on that `n` and feed it to `f`. -So the "Option monad" consists of the polymorphic option type, the -unit function, and the bind function. +So the "option monad" consists of the polymorphic option type, the +unit function, and the bind function. With the option monad, we can +think of the "safe division" operation -A note on notation: some people use the infix operator `>==` to stand +
+# let divide num den = if den = 0 then None else Some (num/den);; +val divide : int -> int -> int option =+ +as basically a function from two integers to an integer, except with +this little bit of option frill, or option plumbing, on the side. + +A note on notation: Haskell uses the infix operator `>>=` to stand for `bind`. I really hate that symbol. Following Wadler, I prefer to infix five-pointed star, or on a keyboard, `*`. @@ -110,40 +119,63 @@ them from hurting the people that use them or themselves. val ( * ) : 'a option -> ('a -> 'b option) -> 'b option =+
-Some 3 * unit * unit;; +# Some 3 * unit * unit;; - : int option = Some 3 -Some 3 * (fun x -> unit x * unit);; +# Some 3 * (fun x -> unit x * unit);; - : int option = Some 3 + +# Some 3 * divide 6 * divide 2;; +- : int option = Some 1 +# Some 3 * (fun x -> divide 6 x * divide 2);; +- : int option = Some 1 + +# Some 3 * divide 2 * divide 6;; +- : int option = None +# Some 3 * (fun x -> divide 2 x * divide 6);; +- : int option = None- Of course, associativity must hold for arbitrary functions of - type `'a -> M 'a`, where `M` is the monad type. It's easy to - convince yourself that the bind operation for the option monad - obeys associativity by dividing the inputs into cases: if `m` - matches `None`, both computations will result in `None`; if - `m` matches `Some n`, and `f n` evalutes to `None`, then both - computations will again result in `None`; and if the value of - `f n` matches `Some r`, then both computations will evaluate - to `g r`. +Of course, associativity must hold for arbitrary functions of +type `'a -> M 'a`, where `M` is the monad type. It's easy to +convince yourself that the bind operation for the option monad +obeys associativity by dividing the inputs into cases: if `m` +matches `None`, both computations will result in `None`; if +`m` matches `Some n`, and `f n` evalutes to `None`, then both +computations will again result in `None`; and if the value of +`f n` matches `Some r`, then both computations will evaluate +to `g r`. * Right identity: unit is a right identity for bind. That is, `m * unit == m` for all monad objects `m`. For instance, @@ -151,6 +183,8 @@ Some 3 * (fun x -> unit x * unit);;
# Some 3 * unit;; - : int option = Some 3 +# None * unit;; +- : 'a option = NoneNow, if you studied algebra, you'll remember that a *monoid* is an @@ -164,7 +198,7 @@ arguments of a monoid operation) the two arguments of the bind are of different types. But if we generalize bind so that both arguments are of type `'a -> M 'a`, then we get plain identity laws and associativity laws, and the monad laws are exactly like the monoid -laws (see