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:
<pre>
Axiom: ---------
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:
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:
+
+<pre>
+------------------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
+</pre>
+
+With labels, we have
+
+<pre>
+------------------------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
+</pre>
+
+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`.
+
+<pre>
+-----------------------------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
+</pre>
+
+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
+
+<pre>
+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.
+</pre>
+
+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
+
+<pre>
+-----------------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
+</pre>
+
+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...]
--- /dev/null
+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):
+
+<pre>
+# fun f z -> z;;
+- : 'a -> 'b -> 'b = <fun>
+# fun f z -> f 1 z;;
+- : (int -> 'a -> 'b) -> 'a -> 'b = <fun>
+# fun f z -> f 2 (f 1 z);;
+- : (int -> 'a -> 'a) -> 'a -> 'a = <fun>
+# fun f z -> f 3 (f 2 (f 1 z))
+- : (int -> 'a -> 'a) -> 'a -> 'a = <fun>
+</pre>
+
+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)) ~~> <fun>
+
+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.
+