(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..b8c6bf3 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -1,3 +1,5 @@
+[[!toc]]
+

 # System F and recursive types
 
 In the simply-typed lambda calculus, we write types like <code>&sigma;
 # 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.
 
 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>    
 
 
 <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.  
 
 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.]
  
 [See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
 Press, chapter 23.]