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:
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
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