index f6f7ab6..b8c6bf3 100644 (file)
@@ -1,3 +1,5 @@
+[[!toc]]
+
# System F and recursive types

In the simply-typed lambda calculus, we write types like <code>&sigma;
@@ -77,10 +79,11 @@ tick marks, Grecification, or capitalization), there is no need to
distinguish expression abstraction from type abstraction by also
changing the shape of the lambda.

-This expression is a polymorphic version of the identity function.  It
-defines one general identity function that can be adapted for use with
-expressions of any type. In order to get it ready to apply this
-identity function to, say, a variable of type boolean, just do this:
+The expression immediately below is a polymorphic version of the
+identity function.  It defines one general identity function that can
+be adapted for use with expressions of any type. In order to get it
+ready to apply this identity function to, say, a variable of type
+boolean, just do this:

<code>(&Lambda; 'a (&lambda; x:'a . x)) [t]</code>

@@ -115,13 +118,14 @@ System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
relevant evaluator is called "fullpoly"):

N = All X . (X->X)->X->X;
-    Pair = All X . (N -> N -> X) -> X;
+    Pair = (N -> N -> N) -> N;
let zero = lambda X . lambda s:X->X . lambda z:X. z in
+    let fst = lambda x:N . lambda y:N . x 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 pair = lambda x:N . lambda y:N . lambda z:N->N->N . 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
+    let shift = lambda p:Pair . pair (suc (p fst)) (p fst) in
+    let pre = lambda n:N . n [Pair] shift (pair zero zero) snd in

pre (suc (suc (suc zero)));

@@ -132,27 +136,41 @@ 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.
-
+The key to the extra expressive power provided by System F is evident
+in the typing imposed by the definition of `pre`.  The variable `n` is
+typed as a Church number, i.e., as `All X . (X->X)->X->X`.  The type
+application `n [Pair]` instantiates `n` in a way that allows it to
+manipulate ordered pairs: `n [Pair]: (Pair->Pair)->Pair->Pair`.  In
+other words, the instantiation turns a Church number into a
+pair-manipulating function, which is the heart of the strategy for
+this version of predecessor.
+
+Could we try to build a system for doing Church arithmetic in which
+the type for numbers always manipulated ordered pairs?  The problem is
+that the ordered pairs we need here are pairs of numbers.  If we tried
+to replace the type for Church numbers with a concrete (simple) type,
+we would have to replace each `X` with the type for Pairs, `(N -> N ->
+N) -> N`.  But then we'd have to replace each of these `N`'s with the
+type for Church numbers, `(X -> X) -> X -> X`.  And then we'd have to
+replace each of these `X`'s with... ad infinitum.  If we had to choose
+a concrete type built entirely from explicit base types, we'd be
+unable to proceed.
[See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
-Press, pp. 350--353, for `tail` for lists in System F.]
+Press, chapter 23.]

Typing &omega;
--------------

-In fact, it is even possible to give a type for &omega; in System F.
+In fact, unlike in the simply-typed lambda calculus,
+it is even possible to give a type for &omega; in System F.

<code>&omega; = lambda x:(All X. X->X) . x [All X . X->X] x</code>

In order to see how this works, we'll apply &omega; to the identity
function.

-<code>&omega; [All X . X -> X] id ==</code>
+<code>&omega; id ==</code>

(lambda x:(All X . X->X) . x [All X . X->X] x) (lambda X . lambda x:X . x)

@@ -161,11 +179,11 @@ right type to serve as the argument to &omega;.  The definition of
&omega; instantiates the identity function by binding the type
variable `X` to the universal type `All X . X->X`.  Instantiating the
identity function in this way results in an identity function whose
-type is the same as the original fully polymorphic identity function.
+type is (in some sense, only accidentally) the same as the original
+fully polymorphic identity function.

So in System F, unlike in the simply-typed lambda calculus, it *is*
-possible for a function (in this case, the identity function) to apply
-to itself!
+possible for a function to apply to itself!

Does this mean that we can implement recursion in System F?  Not at
all.  In fact, despite its differences with the simply-typed lambda
@@ -177,8 +195,9 @@ form in a finite number of steps.
Not only does a fixed-point combinator remain out of reach, we can't
even construct an infinite loop.  This means that although we found a
type for &omega;, there is no general type for &Omega; &equiv; &omega;
-&omega;.  (It turns out that no Turing complete system can be strongly
-normalizing, from which it follows that System F is not Turing complete.)
+&omega;.  Furthermore, it turns out that no Turing complete system can
+be strongly normalizing, from which it follows that System F is not
+Turing complete.

Types in OCaml