X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=list_monad_as_continuation_monad.mdwn;h=e4772f88888a50876a370d8af6c53d88ad1da608;hp=0edec2552c4f1b0fa6bf6238dd9864b9cfc0fc56;hb=49e6889d3ceb77526298a84549df44871caaf7a0;hpb=c51397c5a41cbf75e37382905b212868e427b16b diff --git a/list_monad_as_continuation_monad.mdwn b/list_monad_as_continuation_monad.mdwn index 0edec255..e4772f88 100644 --- 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: - ... 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+(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)) ~~> @@ -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