Then our unit is naturally:
- let s_unit (x : 'a) : ('a state) = fun (s : store) -> (x, s)
+ let s_unit (a : 'a) : ('a state) = fun (s : store) -> (a, s)
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:
looks like this:
type 'a list = ['a];;
- l_unit (x : 'a) = [x];;
+ l_unit (a : 'a) = [a];;
l_bind u f = List.concat (List.map f u);;
Recall that `List.map` take a function and a list and returns the
into OCaml lists soon. We don't need to fully grasp the role of the `'b`'s
in order to proceed to build a monad:
- l'_unit (x : 'a) : ('a, 'b) list = fun x -> fun f z -> f x z
+ l'_unit (a : 'a) : ('a, 'b) list = fun a -> fun f z -> f a z
No problem. Arriving at bind is a little more complicated, but
exactly the same principles apply, you just have to be careful and
Let's write a general function that will map individuals into their
corresponding generalized quantifier:
- gqize (x : e) = fun (p : e -> t) -> p x
+ gqize (a : e) = fun (p : e -> t) -> p a
This function wraps up an individual in a fancy box. That is to say,
we are in the presence of a monad. The type constructor, the unit and
similar to the List monad just given:
type 'a continuation = ('a -> 'b) -> 'b
- c_unit (x : 'a) = fun (p : 'a -> 'b) -> p x
+ c_unit (a : 'a) = fun (p : 'a -> 'b) -> p a
c_bind (u : ('a -> 'b) -> 'b) (f : 'a -> ('c -> 'd) -> 'd) : ('c -> 'd) -> 'd =
- fun (k : 'a -> 'b) -> u (fun (x : 'a) -> f x k)
+ fun (k : 'a -> 'b) -> u (fun (a : 'a) -> f a k)
How similar is it to the List monad? Let's examine the type
constructor and the terms from the list monad derived above:
type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
- l'_unit x = fun f -> f x
- l'_bind u f = fun k -> u (fun x -> f x k)
+ l'_unit a = fun f -> f a
+ l'_bind u f = fun k -> u (fun a -> f a k)
(We performed a sneaky but valid eta reduction in the unit term.)