```-# fun f z -> z;;
-- : 'a -> 'b -> 'b =
-# fun f z -> f 1 z;;
-- : (int -> 'a -> 'b) -> 'a -> 'b =
-# fun f z -> f 2 (f 1 z);;
-- : (int -> 'a -> 'a) -> 'a -> 'a =
-# fun f z -> f 3 (f 2 (f 1 z))
-- : (int -> 'a -> 'a) -> 'a -> 'a =
-```
```-# let cons h t = h :: t;;  (* Ocaml is stupid about :: *)
-# l'_bind (fun f z -> f 1 (f 2 z))
-          (fun i -> fun f z -> f i (f (i+1) z)) cons [];;
-- : int list = [1; 2; 2; 3]
-```
+ # let cons h t = h :: t;; (* OCaml is stupid about :: *) + # l'_bind (fun f z -> f 1 (f 2 z)) + (fun i -> fun f z -> f i (f (i+1) z)) cons [];; + - : int list = [1; 2; 2; 3] Ta da! @@ -263,7 +299,7 @@ generalized quantifier `fun pred -> pred j` of type `(e -> t) -> t`. 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 @@ -271,19 +307,17 @@ the bind follow naturally. We've done this enough times that we won't belabor the construction of the bind function, the derivation is similar to the List monad just given: -
```-type 'a continuation = ('a -> 'b) -> 'b
-c_unit (x:'a) = fun (p:'a -> 'b) -> p x
-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)
-```