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:
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 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
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
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:
As usual, we need to unpack the `u` box. Examine the type of `u`.
This time, `u` will only deliver up its contents if we give `u` an
argument that is a function expecting an `'a` and a `'b`. `u` will
-fold that function over its type `'a` members, and that's how we'll get the `'a`s we need. Thus:
+fold that function over its type `'a` members, and that's where we can get at the `'a`s we need. Thus:
... u (fun (a : 'a) (b : 'b) -> ... f a ... ) ...
-In order for `u` to have the kind of argument it needs, 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 ... ) ...
-Now we have an argument `b` of type `'b`, so we can supply that to `(f a) k`, getting a result of type `'b`, as we need:
+Now the function we're supplying to `u` also receives an argument `b` of type `'b`, so we can supply that to `f a k`, getting a result of type `'b`, as we need:
... u (fun (a : 'a) (b : 'b) -> f a k b) ...
Suppose we have a list' whose contents are `[1; 2; 4; 8]`---that is, our list' will be `fun f z -> f 1 (f 2 (f 4 (f 8 z)))`. We call that list' `u`. Suppose we also have a function `f` that for each `int` we give it, gives back a list of the divisors of that `int` that are greater than 1. Intuitively, then, binding `u` to `f` should give us:
- concat (map f u) =
- concat [[]; [2]; [2; 4]; [2; 4; 8]] =
+ List.concat (List.map f u) =
+ List.concat [[]; [2]; [2; 4]; [2; 4; 8]] =
[2; 2; 4; 2; 4; 8]
Or rather, it should give us a list' version of that, which takes a function `k` and value `z` as arguments, and returns the right fold of `k` and `z` over those elements. What does our formula
So if, for example, we let `k` be `+` and `z` be `0`, then the computation would proceed:
0 ==>
- right-fold + and 0 over [2; 4; 8] = ((2+4+8+0) ==>
- right-fold + and 2+4+8+0 over [2; 4] = 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))
+ right-fold + and 0 over [2; 4; 8] = 2+4+8+(0) ==>
+ right-fold + and 2+4+8+0 over [2; 4] = 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
-will deliver just the same folds, for arbitrary choices of `k` and `z` (with the right types), and arbitrary list's `u` and appropriately-typed `f`s, as
+will deliver just the same folds, for arbitrary choices of `k` and `z` (with the right types), and arbitrary `list'`s `u` and appropriately-typed `f`s, as
- fun k z -> List.fold_right k (concat (map f u)) z
+ fun k z -> List.fold_right k (List.concat (List.map f u)) z
would.
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>
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