X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=zipper-lists-continuations.mdwn;h=581cdf4e77fe669e9cd37f512d70fea2cb29d4fe;hp=1b571f616bd9a250e669ecfe1f6b35138a6d373b;hb=051c4bc23f4c1107423d50d370e15ef723187b03;hpb=48a42d03d6e2562628e1ab9cc7e134cc9bcf4294 diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn index 1b571f61..581cdf4e 100644 --- a/zipper-lists-continuations.mdwn +++ b/zipper-lists-continuations.mdwn @@ -5,7 +5,7 @@ continuation monad. The three approches are: -[[toc]] +[[!toc]] Rethinking the list monad ------------------------- @@ -26,10 +26,10 @@ constructor is then we can deduce the unit and the bind: - runit x:'a -> 'a reader = fun (e:env) -> x + r_unit x:'a -> 'a reader = fun (e:env) -> x Since the type of an `'a reader` is `fun e:env -> 'a` (by definition), -the type of the `runit` function is `'a -> e:env -> 'a`, which is a +the type of the `r_unit` function is `'a -> e:env -> 'a`, which is a specific case of the type of the *K* combinator. So it makes sense that *K* is the unit for the reader monad. @@ -43,18 +43,19 @@ We can deduce the correct `bind` function as follows: We have to open up the `u` box and get out the `'a` object in order to feed it to `f`. Since `u` is a function from environments to -objects of type `'a`, we'll have +objects of type `'a`, the way we open a box in this monad is +by applying it to an environment: .... f (u e) ... This subexpression types to `'b reader`, which is good. The only -problem is that we don't have an `e`, so we have to abstract over that -variable: +problem is that we invented an environment `e` that we didn't already have , +so we have to abstract over that variable to balance the books: fun e -> f (u e) ... This types to `env -> 'b reader`, but we want to end up with `env -> -'b`. The easiest way to turn a 'b reader into a 'b is to apply it to +'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 @@ -228,10 +229,12 @@ Sigh. Ocaml won't show us our own list. So we have to choose an `f` and a `z` that will turn our hand-crafted lists into standard Ocaml lists, so that they will print out. +
 # 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! @@ -302,3 +305,6 @@ versa. The connections will be expecially relevant when we consider indefinites and Hamblin semantics on the linguistic side, and non-determinism on the list monad side. +Refunctionalizing zippers +------------------------- +