... f (u e) ... -This subexpression types to `'b reader`, which is good. The only problem is that we made use of an environment `e` that we didn't already have, @@ -63,9 +61,7 @@ and using the Curry-Howard labeling of the proof as our bind term.] This types to `env -> 'b reader`, but we want to end up with `env -> 'b`. Once again, the easiest way to turn a `'b reader` into a `'b` is to apply it to an environment. So we end up as follows: -

-r_bind (u : 'a reader) (f : 'a -> 'b reader) : ('b reader) = f (u e) e -+ r_bind (u : 'a reader) (f : 'a -> 'b reader) : ('b reader) = f (u e) e And we're done. This gives us a bind function of the right type. We can then check whether, in combination with the unit function we chose, it satisfies the monad laws, and behaves in the way we intend. And it does. @@ -84,20 +80,20 @@ Then our unit is naturally: And we can reason our way to the bind function in a way similar to the reasoning given above. First, we need to apply `f` to the contents of the `u` box: - let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state = - ... f (...) ... + let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state = + ... f (...) ... But unlocking the `u` box is a little more complicated. As before, we -need to posit a state `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 +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) ... Abstracting over the `s` and adjusting the types gives the result: - let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state = - fun (s : store) -> let (a, s') = u s in f a s' + let s_bind (u : 'a state) (f : 'a -> 'b state) : 'b state = + fun (s : store) -> let (a, s') = u s in f a s' The **Option/Maybe Monad** doesn't follow the same pattern so closely, so we won't pause to explore it here, though conceptually its unit and bind @@ -123,7 +119,7 @@ boundaries: List.concat [[1; 2]; [2; 3]] ~~> [1; 2; 2; 3] -And sure enough, +And sure enough, l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3] @@ -145,7 +141,7 @@ the object returned by the second argument of `bind` to always be of type `'b list list`. We can elimiate that restriction by flattening the list of lists into a single list: this is just List.concat applied to the output of List.map. So there is some logic to the -choice of unit and bind for the list monad. +choice of unit and bind for the list monad. Yet we can still desire to go deeper, and see if the appropriate bind behavior emerges from the types, as it did for the previously @@ -222,7 +218,7 @@ paragraph much easier to follow.] 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 +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: ... u (fun (a : 'a) (b : 'b) -> ... f a ... ) ... @@ -243,7 +239,7 @@ This whole expression has type `('c -> 'b -> 'b) -> 'b -> 'b`, which is exactly l'_bind (u : ('a -> 'b -> 'b) -> 'b -> 'b) (f : 'a -> ('c -> 'b -> 'b) -> 'b -> 'b) - : ('c -> 'b -> 'b) -> 'b -> 'b = + : ('c -> 'b -> 'b) -> 'b -> 'b = fun k -> u (fun a b -> f a k b) That is a function of the right type for our bind, but to check whether it works, we have to verify it (with the unit we chose) against the monad laws, and reason whether it will have the right behavior. @@ -263,7 +259,7 @@ Suppose we have a list' whose contents are `[1; 2; 4; 8]`---that is, our list' w 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 fun k z -> u (fun a b -> f a k b) z - + do? Well, for each element `a` in `u`, it applies `f` to that `a`, getting one of the lists: [] @@ -300,7 +296,7 @@ Let's make some more tests: l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3] - l'_bind (fun f z -> f 1 (f 2 z)) + l'_bind (fun f z -> f 1 (f 2 z)) (fun i -> fun f z -> f i (f (i+1) z)) ~~>