From 293b63f453994f8c3c458ca264ef0fb04b79e1fb Mon Sep 17 00:00:00 2001
From: Chris
Date: Thu, 26 Feb 2015 13:24:58 0500
Subject: [PATCH] edits

topics/_week5_system_F.mdwn  66 +++++++++++++++++++++
1 file changed, 30 insertions(+), 36 deletions()
diff git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 4bde11e0..4517509b 100644
 a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ 51,16 +51,16 @@ Then System F can be specified as follows:
In the definition of the types, "`c`" is a type constant. Type
constants play the role in System F that base types play in the
simplytyped 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 variables
can be distinguished by using letters from the greek alphabet
(α, β, etc.), or by using capital roman letters (X, Y,
etc.). "`Ï1 > Ï2`" is the type of a function from expressions of
type `Ï1` to expressions of type `Ï2`. And "`âÎ±.Ï`" is called a
universal type, since it universally quantifies over the type variable
`'a`. You can expect that in `âÎ±.Ï`, the type `Ï` will usually
have at least one free occurrence of `Î±` somewhere inside of it.
+constants might include `e` and `t`. "Î±" is a type variable. In
+various discussions, type variables are distinguished by using letters
+from the greek alphabet (α, β, etc.), as we do here, or by
+using capital roman letters (X, Y, etc.), or by adding a tick mark
+(`'a`, `'b`, etc.), as in OCaml. "`Ï1 > Ï2`" is the type of a
+function from expressions of type `Ï1` to expressions of type `Ï2`.
+And "`âÎ±.Ï`" is called a universal type, since it universally
+quantifies over the type variable `α`. You can expect that in
+`âÎ±.Ï`, the type `Ï` will usually 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 simplytyped lambda
@@ 79,24 +79,19 @@ variables. So in the expression
Λ Î± (λ x:Î±. x)
the Λ
binds the type variable `Î±` that occurs in
the λ
abstract. Of course, as long as type
variables are carefully distinguished from expression variables (by
tick marks, Grecification, or capitalization), there is no need to
distinguish expression abstraction from type abstraction by also
changing the shape of the lambda.

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:
+the λ
abstract.
+
+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:
(Λ Î± (λ x:Î±. x)) [t]
This type application (where `t` is a type constant for Boolean truth
values) specifies the value of the type variable `Î±`. Not
surprisingly, the type of this type application is a function from
Booleans to Booleans:
+surprisingly, the type of the expression that results from this type
+application is a function from Booleans to Booleans:
((ΛÎ± (λ x:Î± . x)) [t]): (b>b)
@@ 111,20 +106,17 @@ instantiated as a function from expresions of type `Î±` to expressions
of type `Î±`. In general, then, the type of the uninstantiated
(polymorphic) identity function is
(ΛÎ± (λx:Î± . x)): (∀Î±. Î±Î±)
+(ΛÎ± (λx:Î± . x)): (∀Î±. Î±>Î±)
Pred in System F

We saw that the predecessor function couldn't be expressed in the
simplytyped lambda calculus. It *can* be expressed in System F,
however. Here is one way, coded in
[[Benjamin Pierce's typechecker and evaluator for
System Fhttp://www.cis.upenn.edu/~bcpierce/tapl/index.html]] (the
relevant evaluator is called "fullpoly"):
+however. Here is one way:
 N = âÎ±.(Î±>Î±)>Î±>Î±;
 Pair = (N>N>N)>N;
+ let N = âÎ±.(Î±>Î±)>Î±>Î± in
+ let Pair = (N>N>N)>N in
let zero = ÎÎ±. Î»s:Î±>Î±. Î»z:Î±. z in
let fst = Î»x:N. Î»y:N. x in
@@ 136,12 +128,14 @@ relevant evaluator is called "fullpoly"):
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 typelevel
lambda, though the difference is encoded in whether the variables are
lower case (for ordinary lambda) or upper case (for typelevel
lambda).
+[If you want to run this code in
+[[Benjamin Pierce's typechecker and evaluator for
+System Fhttp://www.cis.upenn.edu/~bcpierce/tapl/index.html]], the
+relevant evaluator is called "fullpoly", and you'll need to
+truncate the names of "suc(c)" and "pre(d)", since those are
+reserved words in Pierce's system.]
+
+Exercise: convince yourself that `zero` has type `N`.
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

2.11.0