(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 6b80c20..f753709 100644 (file)
--- a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ -34,8 +34,7 @@ notational convention (which will last throughout the rest of the
 course) that "<code>x:&alpha;</code>" represents an expression `x`
 whose type is <code>&alpha;</code>.
 
 course) that "<code>x:&alpha;</code>" represents an expression `x`
 whose type is <code>&alpha;</code>.
 

-Then System F can be specified as follows (choosing notation that will
-match up with usage in O'Caml, whose type system is based on System F):
+Then System F can be specified as follows:

 
        System F:
        ---------
 
        System F:
        ---------


@@ -47,7 +46,7 @@ constants play the role in System F that base types play in the
 simply-typed lambda calculus.  So in a lingusitics context, type
 constants might include `e` and `t`.  "α" is a type variable.  The
 tick mark just indicates that the variable ranges over types rather
 simply-typed lambda calculus.  So in a lingusitics context, type
 constants might include `e` and `t`.  "α" is a type variable.  The
 tick mark just indicates that the variable ranges over types rather

-than over values; in various discussion below and later, type variable
+than over values; in various discussion below and later, type variables

 can be distinguished by using letters from the greek alphabet
 (&alpha;, &beta;, etc.), or by using capital roman letters (X, Y,
 etc.).  "`τ1 -> τ2`" is the type of a function from expressions of
 can be distinguished by using letters from the greek alphabet
 (&alpha;, &beta;, etc.), or by using capital roman letters (X, Y,
 etc.).  "`τ1 -> τ2`" is the type of a function from expressions of


@@ -57,7 +56,7 @@ universal type, since it universally quantifies over the type variable
 have at least one free occurrence of `α` somewhere inside of it.
 
 In the definition of the expressions, we have variables "`x`" as usual.
 have at least one free occurrence of `α` somewhere inside of it.
 
 In the definition of the expressions, we have variables "`x`" as usual.

-Abstracts "`λx:τ. e`" are similar to abstracts in the simply-typed lambda
+Abstracts "`λx:τ.e`" are similar to abstracts in the simply-typed lambda

 calculus, except that they have their shrug variable annotated with a
 type.  Applications "`e1 e2`" are just like in the simply-typed lambda calculus.
 
 calculus, except that they have their shrug variable annotated with a
 type.  Applications "`e1 e2`" are just like in the simply-typed lambda calculus.
 


@@ -117,15 +116,15 @@ however.  Here is one way, coded in
 System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
 relevant evaluator is called "fullpoly"):
 
 System F|http://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
 relevant evaluator is called "fullpoly"):
 

-    N = ∀α. (α->α)->α->α;
-    Pair = (N->N->N) -> N;
-    let zero = α . λs:α->α . λz:α. z in 
-    let fst = λx:N . λy:N . x in
-    let snd = λx:N . λy:N . y in
-    let pair = λx:N . λy:N . λz:N->N->N . z x y in
-    let suc = λn:N . λα . λlambda s:α->α . λz:α . s (n [α] s z) in
-    let shift = λp:Pair . pair (suc (p fst)) (p fst) in
-    let pre = λn:N . n [Pair] shift (pair zero zero) snd in
+    N = ∀α.(α->α)->α->α;
+    Pair = (N->N->N)->N;
+    let zero = Î\9bα.λs:α->α.λz:α.z in 
+    let fst = λx:N.λy:N.x in
+    let snd = λx:N.λy:N.y in
+    let pair = λx:N.λy:N.λz:N->N->N.z x y in
+    let suc = λn:N.λα.λs:α->α.λz:α.s (n [α] s z) in
+    let shift = λp:Pair.pair (suc (p fst)) (p fst) in
+    let pre = λn:N.n [Pair] shift (pair zero zero) snd in

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


@@ -138,7 +137,7 @@ lambda).
 
 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
 
 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 `∀ α . (α->α)->α->α`.  The type
+typed as a Church number, i.e., as `∀α.(α->α)->α->α`.  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
 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


@@ -165,19 +164,19 @@ Typing &omega;
 In fact, unlike in the simply-typed lambda calculus, 
 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:(∀ α. α->α) . x [∀ α . α->α] x</code>
+<code>&omega; = λx:(∀α.α->α).x [∀α.α->α] x</code>

 
 In order to see how this works, we'll apply &omega; to the identity
 function.  
 
 <code>&omega; id ==</code>
 
 
 In order to see how this works, we'll apply &omega; to the identity
 function.  
 
 <code>&omega; id ==</code>
 

-    (lambda x:(∀ α . α->α) . x [∀ α . α->α] x) (lambda α . lambda x:α . x)
+    (λx:(∀α.α->α). x [∀α.α->α] x) (Λα.λx:α.x)

 
 

-Since the type of the identity function is `(∀ α . α->α)`, it's the
+Since the type of the identity function is `∀α.α->α`, it's the

 right type to serve as the argument to &omega;.  The definition of
 &omega; instantiates the identity function by binding the type
 right type to serve as the argument to &omega;.  The definition of
 &omega; instantiates the identity function by binding the type

-variable `α` to the universal type `∀ α . α->α`.  Instantiating the
+variable `α` to the universal type `∀α.α->α`.  Instantiating the

 identity function in this way results in an identity function whose
 type is (in some sense, only accidentally) the same as the original
 fully polymorphic identity function.
 identity function in this way results in an identity function whose
 type is (in some sense, only accidentally) the same as the original
 fully polymorphic identity function.


@@ -228,10 +227,8 @@ uses.  Can we capture this using polymorphic types?
 
 With these basic types, we want to say something like this:
 
 
 With these basic types, we want to say something like this:
 

-    and:t->t->t = lambda l:t . lambda r:t . l r false
-    and = lambda α . lambda β . 
-            lambda l:α->β . lambda r:α->β . 
-              lambda x:α . and:β (l x) (r x)
+    and:t->t->t = λl:t. λr:t. l r false
+    and = Λα.Λβ.λl:α->β.λr:α->β.λx:α. and [β] (l x) (r x)

 
 The idea is that the basic *and* conjoins expressions of type `t`, and
 when *and* conjoins functional types, it builds a function that
 
 The idea is that the basic *and* conjoins expressions of type `t`, and
 when *and* conjoins functional types, it builds a function that