author Chris Tue, 24 Feb 2015 15:00:01 +0000 (10:00 -0500) committer Chris Tue, 24 Feb 2015 15:00:01 +0000 (10:00 -0500)

index 047ee8b..4caeb55 100644 (file)
@@ -208,32 +208,55 @@ the predecessor of zero should be a number, perhaps zero.)

Rather, the problem is that the definition of the function requires
subterms that can't be simply-typed.  We'll illustrate with our
-implementation of the predecessor, sightly modified in inessential
-ways to suit present purposes:
+implementation of the predecessor function, based on the discussion in
+Pierce 2002:547:

let zero = \s z. z in
let snd = \a b. b in
let pair = \a b. \v. v a b in
let succ = \n s z. s (n s z) in
-    let collect = \p. p (\a b. pair (succ a) a)
-    let pred = \n. n collect (pair zero zero) snd in
+    let shift = \p. p (\a b. pair (succ a) a)
+    let pred = \n. n shift (pair zero zero) snd in
+
+Note that `shift` applies its argument p ("p" for "pair") to a
+function that ignores its second argument---why does it do that?  In
+order to understand what this code is doing, it is helpful to go
+through a sample computation, the predecessor of 3:
+
+    pred (\s z.s(s(s z)))
+    (\s z.s(s(s z))) (\n.n shift (\f.f 0 0) snd)
+    shift (shift (shift (\f.f 0 0))) snd
+    shift (shift ((\f.f 0 0) (\a b.pair(succ a) a))) snd
+    shift (shift (\f.f 1 0)) snd
+    shift (\f. f 2 1) snd
+    (\f. f 3 2) snd
+    2
+
+At each stage, `shift` sees an ordered pair that contains two numbers
+related by the successor function.  It can safely discard the second
+element without losing any information.  The reason we carry around
+the second element at all is that when it comes time to complete the
+computation---that is, when we finally apply the top-level ordered
+pair to `snd`---it's the second element of the pair that will serve as
+the final result.

Let's see how far we can get typing these terms.  `zero` is the Church
encoding of zero.  Using `N` as the type for Church numbers (i.e.,
-<code>N &equiv; (&sigma; -> &sigma;) -> &sigma; -> &sigma;</code> for some
-&sigma;, `zero` has type `N`.  `snd` takes two numbers, and returns
-the second, so `snd` has type `N -> N -> N`.  Then the type of `pair`
-is `N -> N -> (type(snd)) -> N`, that is, `N -> N -> (N -> N -> N) ->
-N`.  Likewise, `succ` has type `N -> N`, and `collect` has type `pair
--> pair`, where `pair` is the type of an ordered pair of numbers,
-namely, <code>pair &equiv; (N -> N -> N) -> N</code>.  So far so good.
+<code>N &equiv; (&sigma; -> &sigma;) -> &sigma; -> &sigma;</code> for
+some &sigma;, `zero` has type `N`.  `snd` takes two numbers, and
+returns the second, so `snd` has type `N -> N -> N`.  Then the type of
+`pair` is `N -> N -> (type(snd)) -> N`, that is, `N -> N -> (N -> N ->
+N) -> N`.  Likewise, `succ` has type `N -> N`, and `shift` has type
+`pair -> pair`, where `pair` is the type of an ordered pair of
+numbers, namely, <code>pair &equiv; (N -> N -> N) -> N</code>.  So far
+so good.

The problem is the way in which `pred` puts these parts together.  In
particular, `pred` applies its argument, the number `n`, to the
-`collect` function.  Since `n` is a number, its type is <code>(&sigma;
+`shift` function.  Since `n` is a number, its type is <code>(&sigma;
-> &sigma;) -> &sigma; -> &sigma;</code>.  This means that the type of
-`collect` has to match <code>&sigma; -> &sigma;</code>. But we
-concluded above that the type of `collect` also had to be `pair ->
+`shift` has to match <code>&sigma; -> &sigma;</code>. But we
+concluded above that the type of `shift` also had to be `pair ->
pair`.  Putting these constraints together, it appears that
<code>&sigma;</code> must be the type of a pair of numbers.  But we
already decided that the type of a pair of numbers is `(N -> N -> N)
@@ -246,7 +269,7 @@ allowed in the simply-typed lambda calculus.
The way we got here is that the `pred` function relies on the built-in
right-fold structure of the Church numbers to recursively walk down
the spine of its argument.  In order to do that, the argument had to
-apply to the `collect` operation.  And since `collect` had to be the
+apply to the `shift` operation.  And since `shift` had to be the
sort of operation that manipulates numbers, the infinite regress is
established.

@@ -259,11 +282,11 @@ Because lists are (in effect) a generalization of the Church numbers,
computing the tail of a list is likewise beyond the reach of the
simply-typed lambda calculus.

-This result is surprising.  It illustrates how recursion is built into
-the structure of the Church numbers (and lists).  Most importantly for
-the discussion of the simply-typed lambda calculus, it demonstrates
-that even fairly basic recursive computations are beyond the reach of
-a simply-typed system.
+This result is not obvious, to say the least.  It illustrates how
+recursion is built into the structure of the Church numbers (and
+lists).  Most importantly for the discussion of the simply-typed
+lambda calculus, it demonstrates that even fairly basic recursive
+computations are beyond the reach of a simply-typed system.

## Montague grammar is based on a simply-typed lambda calculus
index fe451a0..cd1b617 100644 (file)
@@ -96,11 +96,53 @@ Pred in System F
----------------

We saw that the predecessor function couldn't be expressed in the
-simply-typed lambda calculus.  It can be expressed in System F, however.
+simply-typed lambda calculus.  It can be expressed in System F,
+however.  Here is one way, coded in
+[[Benjamin Pierce's type-checker and evaluator for
+System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
+part you want is called "fullpoly"):
+
+    N = All X . (X->X)->X->X;
+    Pair = All X . (N -> N -> X) -> X;
+    let zero = lambda X . lambda s:X->X . lambda z:X. z in
+    let snd = lambda x:N . lambda y:N . y in
+    let pair = lambda x:N . lambda y:N . lambda X . lambda z:N->N->X . z x y in
+    let suc = lambda n:N . lambda X . lambda s:X->X . lambda z:X . s (n [X] s z) in
+    let shift = lambda p:Pair . p [Pair] (lambda a:N . lambda b:N . pair (suc a) a) in
+    let pre = lambda n:N . n [Pair] shift (pair zero zero) [N] snd in
+
+    pre (suc (suc (suc zero)));
+
+We've truncated the names of "suc(c)" and "pre(d)", since those are
+reserved words in Pierce's system.  Note that in this code, there is
+no typographic distinction between ordinary lambda and type-level
+lambda, though the difference is encoded in whether the variables are
+lower case (for ordinary lambda) or upper case (for type-level
+lambda).
+
+The key to the extra flexibility provided by System F is that we can
+instantiate the `pair` function to return a number, as in the
+definition of `pre`, or we can instantiate it to return an ordered
+pair, as in the definition of the `shift` function.  Because we don't
+have to choose a single type for all uses of the pair-building
+function, we aren't forced into a infinite regress of types.

[See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
Press, pp. 350--353, for `tail` for lists in System F.]

+Typing &omega;
+--------------
+
+In fact, it is even possible to give a type for &omeage; in System F.
+
+    omega = lambda x:(All X. X->X) . x [All X . X->X] x in
+    omega;
+
+Each time the internal application is performed, the type of the head
+is chosen anew.  And each time, we choose the same type as before, the
+type of a function that takes an argument of any type and returns a
+result of the same type...
+

Types in OCaml
--------------