From fa3fcd726119256a230682b5125180daefd11235 Mon Sep 17 00:00:00 2001 From: Chris Barker Date: Fri, 26 Nov 2010 23:09:25 -0500 Subject: [PATCH] from zippers to lists to continuations --- curry-howard.mdwn | 170 +++++++++++++++++++++++++-- zipper-lists-continuations.mdwn | 250 ++++++++++++++++++++++++++++++++++++++++ 2 files changed, 413 insertions(+), 7 deletions(-) create mode 100644 zipper-lists-continuations.mdwn diff --git a/curry-howard.mdwn b/curry-howard.mdwn index f3c1be75..6cd08c10 100644 --- a/curry-howard.mdwn +++ b/curry-howard.mdwn @@ -18,13 +18,16 @@ the abstract `\xM` has type σ `-->` τ. If a term `M` has type σ `-->` τ, and a term `N` has type σ, then the application `MN` has type τ. -These rules are clearly obverses of one another: the functional types -that abstract builds up are taken apart by application. +These rules are clearly inverse of one another (in some sense to be +made precise): the functional types that abstract builds up are taken +apart by application. The intuition that abstraction and application +are dual to each other is the heart of the Curry-Howard +correspondence. The next step in making sense out of the Curry-Howard corresponence is to present a logic. It will be a part of intuitionistic logic. We'll -start with the implicational fragment (that is, the part of -intuitionistic logic that only involves axioms and implications): +start with the implicational fragment, that is, the part of +intuitionistic logic that only involves axioms and implications: 
 Axiom: ---------
@@ -116,7 +119,7 @@ labeled formulas, those labels remain unchanged in the conclusion.
 
 What is means for a variable `x` to be chosen *fresh* is that
 `x` must be distinct from any other variable in any of the labels
-used in the proof.
+used in the (sub)proof up to that point.
 
 Using these labeling rules, we can label the proof
 just given:
@@ -134,8 +137,161 @@ x:A |- (\y.x):(B --> A)
 
 We have derived the *K* combinator, and typed it at the same time!
 
-Need a proof that involves application, and a proof with cut that will
-show beta reduction, so "normal" proof.
+In order to make use of the dual rule, the one for `-->` elimination,
+we need a context that will entail both `A --> B` and `A`.  Here's
+one, first without labels: 
+
+
+------------------Axiom          
+A --> B |- A --> B          
+---------------------Weak        ---------Axiom
+A --> B, A |- A --> B              A |- A
+---------------------Exch        -----------------Weak 
+A, A --> B |- A --> B              A, A --> B |- A
+-------------------------------------------------- --> E
+A, A --> B |- B 
+

+
+With labels, we have
+
+
+------------------------Axiom          
+f:A --> B |- f:A --> B          
+----------------------------Weak        -------------Axiom
+f:A --> B, x:A |- f:A --> B              x:A |- x:A
+----------------------------Exch        ------------------------Weak 
+x:A, f:A --> B |- f:A --> B              x:A, f:A --> B |- x:A
+-------------------------------------------------------------- --> E
+x:A, f:A --> B |- (fx):B 
+

+
+Note that in order for the `--> E` rule to apply, the left context and
+the right context (the material to the left of each of the turnstiles)
+must match exactly, in this case, `x:A, f:A --> B`.
+
+At this point, an application to natural language will help provide
+insight.
+Instead of labelling the proof above with the kinds of symbols we
+might use in a program, we'll label it with symbols we might use in an
+English sentence.  Instead of a term `f` with type `A --> B`, we'll
+have the English word `left`; and instead of a term `x` with type `A`,
+we'll have the English word `John`.
+
+
+-----------------------------Axiom          
+left:e --> t |- left:e --> t          
+--------------------------------------Weak        -------------------Axiom
+left:e --> t, John:e |- left:e --> t              John:e |- John:e
+--------------------------------------Exch        --------------------------------Weak 
+John:e, left:e --> t |- left:e --> t              John:e, left:e --> t |- John:e
+---------------------------------------------------------------------------------- --> E
+John:e, left:e --> t |- (left John):t 
+

+
+This proof illustrates how a logic can 
+provide three things that a complete grammar of a natural language
+needs:
+
+* It characterizes which words and expressions can be combined in
+order to form a more complex expression.  For instance, we've
+just seen a proof that "left" can combine with "John".
+
+* It characterizes the type (the syntactic category) of the result.
+In the example, an intransitive verb phrase of type `e --> t` combines
+with a determiner phrase of type `e` to form a sentence of type `t`.
+
+* It characterizes the semantic recipe required to compute the meaning
+  of the complex expression based on the meanings of the parts: the
+  way to compute to meaning of the expression "John left" is to take
+  the function denoted by "left" and apply it to the individual
+  denoted by "John", viz., "(left John)".
+
+This last point is the truly novel and beautiful part, the part
+contributed by the Curry-Howard result.  
+
+[Incidentally, note that this proof also suggests that if we have the
+expressions "John" followed by "left", we also have a determiner
+phrase of type `e`.  If you want to make sure that the contribution of
+each word counts (no weakening), you have to use a resource-sensitive
+approach like Linear Logic or Type Logical Grammar.
+
+In this trivial example, it may not be obvious that anything
+interesting is going on, so let's look at a slightly more complicated
+example, one that combines abstraction with application.
+
+Linguistic assumptions (abundently well-motivated, but we won't pause
+to review the motivations here):
+
+Assumption 1:
+Coordinating conjunctions like *and*, *or*, and *but* require that
+their two arguments must have the same sytnactic type.  Thus we can
+have
+
+
+1. [John left] or [Mary left]     coordination of t 
+2. John [left] or [slept]         coordination of e -> t
+3. [John] or [Mary] left          coordination of e
+etc.
+
+4. *John or left.
+5. *left or Mary slept.
+etc.
+

+
+If the two disjuncts have the same type, the coordination is perfectly
+fine, as (1) through (3) illustrate.  But when the disjuncts don't
+match, as in (4) and (5), the result is ungrammatical (though there
+are examples that may seem to work; each usually has a linguistic
+story that needs to be told). 
+
+In general, then, *and* and *or* are polymorphic, and have the type
+`and:('a -> 'a -> 'a)`.  In the discussion below, we'll use a more
+specific instance to keep the discussion concrete, and to abstract
+away from polymorphism.
+
+Assumption 2:
+Some determiner phrases do not denote an indivdual of type `e`, and
+denote only functions of a higher type, typically `(e -> t) -> t` (the
+type of an (extensional) generalized quantifier).  So *John* has type
+`e`, but *everyone* has type `(e -> t) -> t`.
+
+[Excercise: prove using the logic above that *Everyone left* can have
+`(everyone left)` as its Curry-Howard labeling.]
+
+The puzzle, then, is how it can be possible to coordinate generalized
+quantifier determiner phrases with non-generalized quantifier
+determiner phrases:
+
+1. John and every girl laughed.
+2. Some boy or Mary should leave.
+
+The answer involves reasoning about what it means to be an individual.
+
+Let the type of *or* in this example be `Q -> Q -> Q`, where
+`Q` is the type of a generalized quantifier, i.e, `Q = ((e->t)->t`.
+
+John:e |- John:e, or:(Q->Q->Q) |- , everyone:Q, left:e->t
+
+
+-----------------Ax  -----------------Ax
+John:e |- John:e     P:e->t |- P:e->t
+--------------------------------------Modus Ponens (proved above)
+John:e, P:e->t |- (P John):t
+--------------------------------- --> I
+John:e |- (\P.P John):(e->t)->t
+

+
+This proof is very interesting: it says that if *John* has type `e`,
+then *John* automatically can be used as if it also has type
+`(e->t)->t`, the type of a generalized quantifier.  
+The Curry-Howard labeling is the term `\P.P John`, which is a function
+from verb phrase meanings to truth values, just as we would need.
+
+[John and everyone left]
+
+beta reduction = normal proof.
+
+
 
 [To do: add pairs and destructors; unit and negation...]
 
diff --git a/zipper-lists-continuations.mdwn b/zipper-lists-continuations.mdwn
new file mode 100644
index 00000000..d13dc353
--- /dev/null
+++ b/zipper-lists-continuations.mdwn
@@ -0,0 +1,250 @@
+Today we're going to encounter continuations.  We're going to come at
+them from three different directions, and each time we're going to end
+up at the same place: a particular monad, which we'll call the
+continuation monad.
+
+The three approches are:
+
+*    Rethinking the list monad;
+*    Montague's PTQ treatment of DPs as generalized quantifiers; and
+*    Refunctionalizing zippers (Shan: zippers are defunctionalized continuations);
+
+Rethinking the list monad
+-------------------------
+
+To construct a monad, the key element is to settle on a type
+constructor, and the monad naturally follows from that.  I'll remind
+you of some examples of how monads follow from the type constructor in
+a moment.  This will involve some review of familair material, but
+it's worth doing for two reasons: it will set up a pattern for the new
+discussion further below, and it will tie together some previously
+unconnected elements of the course (more specifically, version 3 lists
+and monads).
+
+For instance, take the **Reader Monad**.  Once we decide that the type
+constructor is
+
+    type 'a reader = fun e:env -> 'a
+
+then we can deduce the unit and the bind:
+
+    runit 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
+specific case of the type of the *K* combinator.  So it makes sense
+that *K* is the unit for the reader monad.
+
+Since the type of the `bind` operator is required to be
+
+    r_bind:('a reader) -> ('a -> 'b reader) -> ('b reader)
+
+We can deduce the correct `bind` function as follows:
+
+    r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) =
+
+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
+
+         .... 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:
+
+         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
+an environment.  So we end up as follows:
+
+    r_bind (u:'a reader) (f:'a -> 'b reader):('b reader) = f (u e) e         
+
+And we're done.
+
+The **State Monad** is similar.  We somehow intuit that we want to use
+the following type constructor:
+
+    type 'a state = 'store -> ('a, 'store)
+
+So our unit is naturally
+
+    let s_unit (x:'a):('a state) = fun (s:'store) -> (x, s)
+
+And we deduce the bind 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) = 
+
+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
+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:state) -> let (a, s') = u s in f a s'
+
+The **Option Monad** doesn't follow the same pattern so closely, so we
+won't pause to explore it here, though conceptually its unit and bind
+follow just as naturally from its type constructor.
+
+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_bind u f = List.concat (List.map f u);;
+
+Recall that `List.map` take a function and a list and returns the
+result to applying the function to the elements of the list:
+
+    List.map (fun i -> [i;i+1]) [1;2] ~~> [[1; 2]; [2; 3]]
+
+and List.concat takes a list of lists and erases the embdded list
+boundaries:
+
+    List.concat [[1; 2]; [2; 3]] ~~> [1; 2; 2; 3]
+
+And sure enough, 
+
+    l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
+
+But where is the reasoning that led us to this unit and bind?
+And what is the type `['a]`?  Magic.
+
+So let's take a *completely useless digressing* and see if we can
+gain some insight into the details of the List monad.  Let's choose
+type constructor that we can peer into, using some of the technology
+we built up so laboriously during the first half of the course.  I'm
+going to use type 3 lists, partly because I know they'll give the
+result I want, but also because they're my favorite.  These were the
+lists that made lists look like Church numerals with extra bits
+embdded in them:
+
+    empty list:                fun f z -> z
+    list with one element:     fun f z -> f 1 z
+    list with two elements:    fun f z -> f 2 (f 1 z)
+    list with three elements:  fun f z -> f 3 (f 2 (f 1 z))
+
+and so on.  To save time, we'll let the Ocaml interpreter infer the
+principle types of these functions (rather than deducing what the
+types should be):
+
+
+# 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 = 
+

+
+Finally, we're getting consistent principle types, so we can stop.
+These types should remind you of the simply-typed lambda calculus
+types for Church numerals (`(o -> o) -> o -> o`) with one extra bit
+thrown in (in this case, and int).
+
+So here's our type constructor for our hand-rolled lists:
+
+    type 'a list' = (int -> 'a -> 'a) -> 'a -> 'a
+
+Generalizing to lists that contain any kind of element (not just
+ints), we have
+
+    type ('a, 'b) list' = ('a -> 'b -> 'b) -> 'b -> 'b
+
+So an `('a, 'b) list'` is a list containing elements of type `'a`,
+where `'b` is the type of some part of the plumbing.  This is more
+general than an ordinary Ocaml list, but we'll see how to map them
+into Ocaml lists soon.  We don't need to 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
+
+No problem.  Arriving at bind is a little more complicated, but
+exactly the same principles apply, you just have to be careful and
+systematic about it.
+
+    l'_bind (u:('a,'b) list') (f:'a -> ('c, 'd) list'): ('c, 'd) list'  = ...
+
+Unfortunately, we'll need to spell out the types:
+
+    l'_bind (u: ('a -> 'b -> 'b) -> 'b -> 'b)
+            (f: 'a -> ('c -> 'd -> 'd) -> 'd -> 'd)
+            : ('c -> 'd -> 'd) -> 'd -> 'd = ...
+
+It's a rookie mistake to quail before complicated types.  You should
+be no more intimiated by complex types than by a linguistic tree with
+deeply embedded branches: complex structure created by repeated
+application of simple rules.
+
+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` as an
+argument a function expecting an `'a`.  Once that argument is applied
+to an object of type `'a`, we'll have what we need.  Thus:
+
+      .... u (fun (x:'a) -> ... (f a) ... ) ...
+
+In order for `u` to have the kind of argument it needs, we have to
+adjust `(f a)` (which has type `('c -> 'd -> 'd) -> 'd -> 'd`) in
+order to deliver something of type `'b -> 'b`.  The easiest way is to
+alias `'d` to `'b`, and provide `(f a)` with an argument of type `'c
+-> 'b -> 'b`.  Thus:
+
+    l'_bind (u: ('a -> 'b -> 'b) -> 'b -> 'b)
+            (f: 'a -> ('c -> 'b -> 'b) -> 'b -> 'b)
+            : ('c -> 'b -> 'b) -> 'b -> 'b = 
+      .... u (fun (x:'a) -> f a k) ...
+
+[Excercise: can you arrive at a fully general bind for this type
+constructor, one that does not collapse `'d`'s with `'b`'s?]
+
+As usual, we have to abstract over `k`, but this time, no further
+adjustments are needed:
+
+    l'_bind (u: ('a -> 'b -> 'b) -> 'b -> 'b)
+            (f: 'a -> ('c -> 'b -> 'b) -> 'b -> 'b)
+            : ('c -> 'b -> 'b) -> 'b -> 'b = 
+      fun (k:'c -> 'b -> 'b) -> u (fun (x:'a) -> f a k)
+
+You should carefully check to make sure that this term is consistent
+with the typing.
+
+Our theory is that this monad should be capable of exactly
+replicating the behavior of the standard List monad.  Let's test:
+
+
+    l_bind [1;2] (fun i -> [i, i+1]) ~~> [1; 2; 2; 3]
+
+    l'_bind (fun f z -> f 1 (f 2 z)) 
+            (fun i -> fun f z -> f i (f (i+1) z)) ~~> 
+
+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!
+
+Just for mnemonic purposes (sneaking in an instance of eta reduction
+to the definition of unit), we can summarize the result as follows:
+
+    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)
+
+To bad this digression, though it ties together various
+elements of the course, has *no relevance whatsoever* to the topic of
+continuations.
+
-- 
2.11.0