From 1758d3493aeb5a8ab805b6cfea11080f72792978 Mon Sep 17 00:00:00 2001 From: Jim Pryor Date: Sat, 27 Nov 2010 20:13:22 -0500 Subject: [PATCH] zipper-lists-contin s/x/a/ Signed-off-by: Jim Pryor --- zipper-lists-continuations.mdwn | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn index 2e84616a..9ef23c25 100644 --- a/zipper-lists-continuations.mdwn +++ b/zipper-lists-continuations.mdwn @@ -73,7 +73,7 @@ The **State Monad** is similar. Once we've decided to use the following type co 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: @@ -100,7 +100,7 @@ Our other familiar monad is the **List Monad**, which we were told 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 @@ -167,7 +167,7 @@ general than an ordinary OCaml list, but we'll see how to map them 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 @@ -299,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 @@ -308,16 +308,16 @@ 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_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.) -- 2.11.0