(no commit message)

[lambda.git] / topics / _week5_system_F.mdwn

diff --git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 2d9035a..72d07b3 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -1,3 +1,5 @@
+[[!toc levels=2]]
+
 # 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>    
 
@@ -142,13 +145,16 @@ 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.  
 
-But of course, the type `Pair` (in this simplified example) is defined
-in terms of Church numbers.  If we tried to replace the type for
-Church numbers with a concrete (simple) type, we would have to replace
-each `X` with `(N -> N -> N) -> N`.  But then we'd have to replace
-each `N` with `(X -> X) -> X -> X`.  And then replace each `X`
-with... ad infinitum.  If we had to choose a concrete type built
-entirely from explicit base types, we'd be unable to proceed.
+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, chapter 23.]
@@ -194,8 +200,8 @@ be strongly normalizing, from which it follows that System F is not
 Turing complete.
 
 
-Types in OCaml
---------------
+#Types in OCaml
+
 
 OCaml has type inference: the system can often infer what the type of
 an expression must be, based on the type of other known expressions.