week7: use u,v for monadic terms

[lambda.git] / week7.mdwn

diff --git a/week7.mdwn b/week7.mdwn
index 9a88221..8b74a1c 100644 (file)
--- a/week7.mdwn
+++ b/week7.mdwn
@@ -53,8 +53,8 @@ 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
                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 it to
-       the option `Some n`.  In the general case, this operation is
+       did this for any integer `x` by mapping it to
+       the option `Some x`.  In the general case, this operation is

        known as `unit` or `return.` Both of those names are terrible. This
        operation is only very loosely connected to the `unit` type we were
        discussing earlier (whose value is written `()`). It's also only
        known as `unit` or `return.` Both of those names are terrible. This
        operation is only very loosely connected to the `unit` type we were
        discussing earlier (whose value is written `()`). It's also only


@@ -87,7 +87,7 @@ that provides at least the following three elements:
        what linguists usually mean by "binding." In our option/maybe monad, the
        bind operation is:
 
        what linguists usually mean by "binding." In our option/maybe monad, the
        bind operation is:
 

-               let bind m f = match m with None -> None | Some n -> f n;;
+               let bind u f = match u with None -> None | Some x -> f x;;

                val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>
 
        Note the type. `bind` takes two arguments: first, a monadic "box"
                val bind : 'a option -> ('a -> 'b option) -> 'b option = <fun>
 
        Note the type. `bind` takes two arguments: first, a monadic "box"


@@ -97,27 +97,27 @@ that provides at least the following three elements:
        and end with bool options).
 
        Intuitively, the interpretation of what `bind` does is like this:
        and end with bool options).
 
        Intuitively, the interpretation of what `bind` does is like this:

-       the first argument is a monadic value m, which 
+       the first argument is a monadic value u, which 

        evaluates to a box that (maybe) contains some ordinary value, call it `x`.
        Then the second argument uses `x` to compute a new monadic
        value.  Conceptually, then, we have
 
        evaluates to a box that (maybe) contains some ordinary value, call it `x`.
        Then the second argument uses `x` to compute a new monadic
        value.  Conceptually, then, we have
 

-               let bind m f = (let x = unbox m in f x);;
+               let bind u f = (let x = unbox u in f x);;

 
        The guts of the definition of the `bind` operation amount to
 
        The guts of the definition of the `bind` operation amount to

-       specifying how to unbox the monadic value `m`.  In the bind
+       specifying how to unbox the monadic value `u`.  In the bind

        opertor for the option monad, we unboxed the option monad by
        opertor for the option monad, we unboxed the option monad by

-       matching the monadic value `m` with `Some n`---whenever `m`
-       happened to be a box containing an integer `n`, this allowed us to
-       get our hands on that `n` and feed it to `f`.
+       matching the monadic value `u` with `Some x`---whenever `u`
+       happened to be a box containing an integer `x`, this allowed us to
+       get our hands on that `x` and feed it to `f`.

 
        If the monadic box didn't contain any ordinary value, then
        we just pass through the empty box unaltered.
 
        In a more complicated case, like our whimsical "singing box" example
        from before, if the monadic value happened to be a singing box
 
        If the monadic box didn't contain any ordinary value, then
        we just pass through the empty box unaltered.
 
        In a more complicated case, like our whimsical "singing box" example
        from before, if the monadic value happened to be a singing box

-       containing an integer `n`, then the `bind` operation would probably
-       be defined so as to make sure that the result of `f n` was also
+       containing an integer `x`, then the `bind` operation would probably
+       be defined so as to make sure that the result of `f x` was also

        a singing box. If `f` also inserted a song, you'd have to decide
        whether both songs would be carried through, or only one of them.
 
        a singing box. If `f` also inserted a song, you'd have to decide
        whether both songs would be carried through, or only one of them.
 


@@ -146,23 +146,23 @@ and Jim feels very uneasy about that. If not `>>=` then we should use
 some other unfamiliar infix symbol (but `>>=` already is such...)
 
 In any case, the course leaders will work this out somehow. In the meantime,
 some other unfamiliar infix symbol (but `>>=` already is such...)
 
 In any case, the course leaders will work this out somehow. In the meantime,

-as you read around, wherever you see `m >>= f`, that means `bind m f`. Also,
+as you read around, wherever you see `u >>= f`, that means `bind u f`. Also,

 if you ever see this notation:
 
        do
 if you ever see this notation:
 
        do

-               x <- m
+               x <- u

                f x
 
                f x
 

-That's a Haskell shorthand for `m >>= (\x -> f x)`, that is, `bind m f`.
+That's a Haskell shorthand for `u >>= (\x -> f x)`, that is, `bind u f`.

 Similarly:
 
        do
 Similarly:
 
        do

-               x <- m
-               y <- n
+               x <- u
+               y <- v

                f x y
 
                f x y
 

-is shorthand for `m >>= (\x -> n >>= (\y -> f x y))`, that is, `bind m (fun x
--> bind n (fun y -> f x y))`. Those who did last week's homework may recognize
+is shorthand for `u >>= (\x -> v >>= (\y -> f x y))`, that is, `bind u (fun x
+-> bind v (fun y -> f x y))`. Those who did last week's homework may recognize

 this.
 
 (Note that the above "do" notation comes from Haskell. We're mentioning it here
 this.
 
 (Note that the above "do" notation comes from Haskell. We're mentioning it here


@@ -183,11 +183,11 @@ The unit/return operation is:
 That is, the simplest way to lift an 'a into an 'a list is just to make a
 singleton list of that 'a. Finally, the bind operation is:
 
 That is, the simplest way to lift an 'a into an 'a list is just to make a
 singleton list of that 'a. Finally, the bind operation is:
 

-       # let bind m f = List.concat (List.map f m);;
+       # let bind u f = List.concat (List.map f u);;

        val bind : 'a list -> ('a -> 'b list) -> 'b list = <fun>
        
        val bind : 'a list -> ('a -> 'b list) -> 'b list = <fun>
        

-What's going on here? Well, consider (List.map f m) first. This goes through all
-the members of the list m. There may be just a single member, if `m = unit a`
+What's going on here? Well, consider (List.map f u) first. This goes through all
+the members of the list u. There may be just a single member, if `u = unit a`

 for some a. Or on the other hand, there may be no members, or many members. In
 any case, we go through them in turn and feed them to f. Anything that gets fed
 to f will be an 'a. f takes those values, and for each one, returns a 'b list.
 for some a. Or on the other hand, there may be no members, or many members. In
 any case, we go through them in turn and feed them to f. Anything that gets fed
 to f will be an 'a. f takes those values, and for each one, returns a 'b list.


@@ -223,7 +223,7 @@ them from hurting the people that use them or themselves.
        a function of type `'a -> 'a m`, so we can use it for `f`:
 
 <pre>
        a function of type `'a -> 'a m`, so we can use it for `f`:
 
 <pre>

-# let ( * ) m f = match m with None -> None | Some n -> f n;;
+# let ( * ) u f = match u with None -> None | Some x -> f x;;

 val ( * ) : 'a option -> ('a -> 'b option) -> 'b option = <fun>
 # let unit x = Some x;;
 val unit : 'a -> 'a option = <fun>
 val ( * ) : 'a option -> ('a -> 'b option) -> 'b option = <fun>
 # let unit x = Some x;;
 val unit : 'a -> 'a option = <fun>


@@ -247,11 +247,11 @@ val unit : 'a -> 'a option = <fun>
 The parentheses is the magic for telling OCaml that the
 function to be defined (in this case, the name of the function
 is `*`, pronounced "bind") is an infix operator, so we write
 The parentheses is the magic for telling OCaml that the
 function to be defined (in this case, the name of the function
 is `*`, pronounced "bind") is an infix operator, so we write

-`m * f` or `( * ) m f` instead of `* m f`.
+`u * f` or `( * ) u f` instead of `* u f`.

 
 *      **Associativity: bind obeys a kind of associativity**. Like this:
 
 
 *      **Associativity: bind obeys a kind of associativity**. Like this:
 

-               (m * f) * g == m * (fun x -> f x * g)
+               (u * f) * g == u * (fun x -> f x * g)

 
        If you don't understand why the lambda form is necessary (the "fun
        x" part), you need to look again at the type of bind.
 
        If you don't understand why the lambda form is necessary (the "fun
        x" part), you need to look again at the type of bind.


@@ -278,15 +278,15 @@ is `*`, pronounced "bind") is an infix operator, so we write
 Of course, associativity must hold for arbitrary functions of
 type `'a -> 'a m`, where `m` is the monad type.  It's easy to
 convince yourself that the bind operation for the option monad
 Of course, associativity must hold for arbitrary functions of
 type `'a -> 'a m`, 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`
+obeys associativity by dividing the inputs into cases: if `u`

 matches `None`, both computations will result in `None`; if
 matches `None`, both computations will result in `None`; if

-`m` matches `Some n`, and `f n` evalutes to `None`, then both
+`u` matches `Some x`, and `f x` evalutes to `None`, then both

 computations will again result in `None`; and if the value of
 computations will again result in `None`; and if the value of

-`f n` matches `Some r`, then both computations will evaluate
-to `g r`.
+`f x` matches `Some y`, then both computations will evaluate
+to `g y`.

 
 *      **Right identity: unit is a right identity for bind.**  That is, 
 
 *      **Right identity: unit is a right identity for bind.**  That is, 

-       `m * unit == m` for all monad objects `m`.  For instance,
+       `u * unit == u` for all monad objects `u`.  For instance,

 
 <pre>
 # Some 3 * unit;;
 
 <pre>
 # Some 3 * unit;;


@@ -303,8 +303,8 @@ If you studied algebra, you'll remember that a *monoid* is an
 associative operation with a left and right identity.  For instance,
 the natural numbers along with multiplication form a monoid with 1
 serving as the left and right identity.  That is, temporarily using
 associative operation with a left and right identity.  For instance,
 the natural numbers along with multiplication form a monoid with 1
 serving as the left and right identity.  That is, temporarily using

-`*` to mean arithmetic multiplication, `1 * n == n == n * 1` for all
-`n`, and `(a * b) * c == a * (b * c)` for all `a`, `b`, and `c`.  As
+`*` to mean arithmetic multiplication, `1 * u == u == u * 1` for all
+`u`, and `(u * v) * w == u * (v * w)` for all `u`, `v`, and `w`.  As

 presented here, a monad is not exactly a monoid, because (unlike the
 arguments of a monoid operation) the two arguments of the bind are of
 different types.  But it's possible to make the connection between
 presented here, a monad is not exactly a monoid, because (unlike the
 arguments of a monoid operation) the two arguments of the bind are of
 different types.  But it's possible to make the connection between


@@ -333,32 +333,32 @@ Here are some of the specifics. You don't have to master these; they're collecte
 
 You may sometimes see:
 
 
 You may sometimes see:
 

-       m >> n
+       u >> v

 
 That just means:
 
 
 That just means:
 

-       m >>= fun _ -> n
+       u >>= fun _ -> v

 
 that is:
 
 
 that is:
 

-       bind m (fun _ -> n)
+       bind u (fun _ -> v)

 
 

-You could also do `bind m (fun x -> n)`; we use the `_` for the function argument to be explicit that that argument is never going to be used.
+You could also do `bind u (fun x -> v)`; we use the `_` for the function argument to be explicit that that argument is never going to be used.

 
 

-The `lift` operation we asked you to define for last week's homework is a common operation. The second argument to `bind` converts 'a values into `b m values---that is, into instances of the monadic type. What if we instead had a function that merely converts `a values into `b values, and we want to use it with our monadic type. Then we "lift" that function into an operation on the monad. For example:
+The `lift` operation we asked you to define for last week's homework is a common operation. The second argument to `bind` converts `'a` values into `'b m` values---that is, into instances of the monadic type. What if we instead had a function that merely converts `'a` values into `'b` values, and we want to use it with our monadic type. Then we "lift" that function into an operation on the monad. For example:

 
        # let even x = (x mod 2 = 0);;
        val g : int -> bool = <fun>
 
 `even` has the type int -> bool. Now what if we want to convert it into an operation on the option/maybe monad?
 
 
        # let even x = (x mod 2 = 0);;
        val g : int -> bool = <fun>
 
 `even` has the type int -> bool. Now what if we want to convert it into an operation on the option/maybe monad?
 

-       # let lift g = fun m -> bind m (fun x -> Some (g x));;
+       # let lift g = fun u -> bind u (fun x -> Some (g x));;

        val lift : ('a -> 'b) -> 'a option -> 'b option = <fun>
 
 `lift even` will now be a function from `int option`s to `bool option`s. We can
 also define a lift operation for binary functions:
 
        val lift : ('a -> 'b) -> 'a option -> 'b option = <fun>
 
 `lift even` will now be a function from `int option`s to `bool option`s. We can
 also define a lift operation for binary functions:
 

-       # let lift2 g = fun m n -> bind m (fun x -> bind n (fun y -> Some (g x y)));;
+       # let lift2 g = fun u v -> bind u (fun x -> bind v (fun y -> Some (g x y)));;

        val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option = <fun>
 
 `lift (+)` will now be a function from `int option`s  and `int option`s to `int option`s. This should look familiar to those who did the homework.
        val lift2 : ('a -> 'b -> 'c) -> 'a option -> 'b option -> 'c option = <fun>
 
 `lift (+)` will now be a function from `int option`s  and `int option`s to `int option`s. This should look familiar to those who did the homework.


@@ -404,15 +404,15 @@ That is the `join` operation.
 
 All of these operations can be defined in terms of `bind` and `unit`; or alternatively, some of them can be taken as primitive and `bind` can be defined in terms of them. Here are various interdefinitions:
 
 
 All of these operations can be defined in terms of `bind` and `unit`; or alternatively, some of them can be taken as primitive and `bind` can be defined in terms of them. Here are various interdefinitions:
 

-       lift f m = ap (unit f) m
-       lift2 f m n = ap (lift f m) n = ap (ap (unit f) m) n
-       ap m n = lift2 id m n
-       lift f m = m >>= compose unit f
-       lift f m = ap (unit f) m
+       lift f u = ap (unit f) u
+       lift2 f u v = ap (lift f u) v = ap (ap (unit f) u) v
+       ap u v = lift2 id u v
+       lift f u = u >>= compose unit f
+       lift f u = ap (unit f) u

        join m2 = m2 >>= id
        join m2 = m2 >>= id

-       m >>= f = join (lift f m)
-       m >> n = m >>= (fun _ -> n)
-       m >> n = lift2 (fun _ -> id) m n
+       u >>= f = join (lift f u)
+       u >> v = u >>= (fun _ -> v)
+       u >> v = lift2 (fun _ -> id) u v

 
 
 
 
 
 


@@ -541,7 +541,7 @@ as an argument.
 Let's test compliance with the left identity law:
 
 <pre>
 Let's test compliance with the left identity law:
 
 <pre>

-# let bind m f (w:s) = f (m w) w;;
+# let bind u f (w:s) = f (u w) w;;

 val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b = <fun>
 # bind (unit 'a') unit 1;;
 - : char = 'a'
 val bind : (s -> 'a) -> ('a -> s -> 'b) -> s -> 'b = <fun>
 # bind (unit 'a') unit 1;;
 - : char = 'a'