index 0edec25..e4772f8 100644 (file)
@@ -88,7 +88,7 @@ need to posit a store `s` that we can apply `u` to.  Once we do so,
however, we won't have an `'a`; we'll have a pair whose first element
is an `'a`.  So we have to unpack the pair:

-       ... let (a, s') = u s in ... (f a) ...
+       ... let (a, s') = u s in ... f a ...

Abstracting over the `s` and adjusting the types gives the result:

@@ -112,7 +112,7 @@ will provide a connection with continuations.
Recall that `List.map` takes a function and a list and returns the
result to applying the function to the elements of the list:

-       List.map (fun i -> [i;i+1]) [1;2] ~~> [[1; 2]; [2; 3]]
+       List.map (fun i -> [i; i+1]) [1; 2] ~~> [[1; 2]; [2; 3]]

and `List.concat` takes a list of lists and erases the embedded list
boundaries:
@@ -121,12 +121,12 @@ boundaries:

And sure enough,

-       l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
+       l_bind [1; 2] (fun i -> [i; i+1]) ~~> [1; 2; 2; 3]

Now, why this unit, and why this bind?  Well, ideally a unit should
not throw away information, so we can rule out `fun x -> []` as an
ideal unit.  And units should not add more information than required,
-so there's no obvious reason to prefer `fun x -> [x;x]`.  In other
+so there's no obvious reason to prefer `fun x -> [x; x]`.  In other
words, `fun x -> [x]` is a reasonable choice for a unit.

As for bind, an `'a list` monadic object contains a lot of objects of
@@ -136,7 +136,7 @@ thing we know for sure we can do with an object of type `'a` is apply
the function of type `'a -> 'a list` to them.  Once we've done so, we
have a collection of lists, one for each of the `'a`'s.  One
possibility is that we could gather them all up in a list, so that
-`bind' [1;2] (fun i -> [i;i]) ~~> [[1;1];[2;2]]`.  But that restricts
+`bind' [1; 2] (fun i -> [i; i]) ~~> [[1; 1]; [2; 2]]`.  But that restricts
the object returned by the second argument of `bind` to always be of
type `'b list list`.  We can eliminate that restriction by flattening
the list of lists into a single list: this is
@@ -198,7 +198,7 @@ Take an `'a` and return its v3-style singleton. No problem.  Arriving at bind
is a little more complicated, but exactly the same principles apply, you just
have to be careful and systematic about it.

-       l'_bind (u : ('a,'b) list') (f : 'a -> ('c, 'd) list') : ('c, 'd) list'  = ...
+       l'_bind (u : ('a, 'b) list') (f : 'a -> ('c, 'd) list') : ('c, 'd) list'  = ...

Unpacking the types gives:

@@ -222,7 +222,7 @@ fold that function over its type `'a` members, and that's where we can get at th

... u (fun (a : 'a) (b : 'b) -> ... f a ... ) ...

-In order for `u` to have the kind of argument it needs, the `fun a b -> ... f a ...` has to have type `'a -> 'b -> 'b`; so the `... f a ...` has to evaluate to a result of type `'b`. The easiest way to do this is to collapse (or "unify") the types `'b` and `'d`, with the result that `f a` will have type `('c -> 'b -> 'b) -> 'b -> 'b`. Let's postulate an argument `k` of type `('c -> 'b -> 'b)` and supply it to `(f a)`:
+In order for `u` to have the kind of argument it needs, the `fun a b -> ... f a ...` has to have type `'a -> 'b -> 'b`; so the `... f a ...` has to evaluate to a result of type `'b`. The easiest way to do this is to collapse (or "unify") the types `'b` and `'d`, with the result that `f a` will have type `('c -> 'b -> 'b) -> 'b -> 'b`. Let's postulate an argument `k` of type `('c -> 'b -> 'b)` and supply it to `f a`:

... u (fun (a : 'a) (b : 'b) -> ... f a k ... ) ...

@@ -276,7 +276,7 @@ So if, for example, we let `k` be `+` and `z` be `0`, then the computation would
right-fold + and 2+4+2+4+8+0 over  = 2+(2+4+(2+4+8+(0))) ==>
right-fold + and 2+2+4+2+4+8+0 over [] = 2+(2+4+(2+4+8+(0)))

-which indeed is the result of right-folding + and 0 over `[2; 2; 4; 2; 4; 8]`. If you trace through how this works, you should be able to persuade yourself that our formula:
+which indeed is the result of right-folding `+` and `0` over `[2; 2; 4; 2; 4; 8]`. If you trace through how this works, you should be able to persuade yourself that our formula:

fun k z -> u (fun a b -> f a k b) z

@@ -292,7 +292,7 @@ For future reference, we might make two eta-reductions to our formula, so that w

Let's make some more tests:

-       l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
+       l_bind [1; 2] (fun i -> [i; i+1]) ~~> [1; 2; 2; 3]

l'_bind (fun f z -> f 1 (f 2 z))
(fun i -> fun f z -> f i (f (i+1) z)) ~~> <fun>
@@ -357,6 +357,8 @@ This can be eta-reduced to:

let l'_unit a = fun k -> k a

+and:
+
let l'_bind u f =
(* we mentioned three versions of this, the fully eta-expanded: *)
fun k z -> u (fun a b -> f a k b) z