fromlists... -> fromlistzippers...

[lambda.git] / list_monad_as_continuation_monad.mdwn

diff --git a/list_monad_as_continuation_monad.mdwn b/list_monad_as_continuation_monad.mdwn
index 0edec25..e4772f8 100644 (file)
--- a/list_monad_as_continuation_monad.mdwn
+++ b/list_monad_as_continuation_monad.mdwn
@@ -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:
 
 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:
 
 
 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:
 
 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:
 
 and `List.concat` takes a list of lists and erases the embedded list
 boundaries:


@@ -121,12 +121,12 @@ boundaries:
 
 And sure enough,
 
 
 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,
 
 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
 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
 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
 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.
 
 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:
 
 
 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 ... ) ...
 
 
        ... 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 ... ) ...
 
 
        ... 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+(2+4+(2+4+8+(0))) ==>
        right-fold + and 2+2+4+2+4+8+0 over [] = 2+(2+4+(2+4+8+(0)))
 
        right-fold + and 2+4+2+4+8+0 over [2] = 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
 
 
        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:
 
 
 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>
        
        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
 
 
        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
        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