X-Git-Url: http://lambda.jimpryor.net/git/gitweb.cgi?p=lambda.git;a=blobdiff_plain;f=topics%2F_week5_system_F.mdwn;h=cd1b6179a31949736fa76ab3473846f434e60b74;hp=fe451a0bb556f6bf5e62287eb1a7433eaff0f85f;hb=de74e6bac683afd7a0d6c64716814ac6c4942c6b;hpb=815520c4c0adc3759fa8dd267ad82f79ed4ab89f

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index fe451a0b..cd1b6179 100644
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -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 ω
+--------------
+
+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
 --------------