From cd52b6efa26b90210609bc266ade1fea3953b6ce Mon Sep 17 00:00:00 2001
From: Chris
Date: Mon, 23 Feb 2015 16:40:54 0500
Subject: [PATCH] edits

topics/_week5_system_F.mdwn  63 ++++++++++++++++++++++++++
1 file changed, 36 insertions(+), 27 deletions()
diff git a/topics/_week5_system_F.mdwn b/topics/_week5_system_F.mdwn
index 2c37ae34..559135e0 100644
 a/topics/_week5_system_F.mdwn
+++ b/topics/_week5_system_F.mdwn
@@ 25,49 +25,55 @@ continuations.)
System F enhances the simplytyped lambda calculus with abstraction
over types. In order to state System F, we'll need to adopt the
notational convention that "x:α
" represents a
expression whose type is α
.
+notational convention that "x:α
" represents an
+expression `x` whose type is α
.
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):
 System F:
+ System F:
+ 
types Ï ::= c  'a  Ï1 > Ï2  â'a. Ï
expressions e ::= x  Î»x:Ï. e  e1 e2  Î'a. e  e [Ï]
In the definition of the types, "`c`" is a type constant (e.g., `e` or
`t`). "`'a`" is a type variable (the tick mark just indicates that
the variable ranges over types rather than values). "`Ï1 > Ï2`" is
the type of a function from expressions of type `Ï1` to expressions of
type `Ï2`. And "`â'a. Ï`" is called a universal type, since it
universally quantifies over the type variable `'a`.

In the definition of the expressions, we have variables "`x`".
+`t`, or in arithmetic contexts, `N` or `Int`). "`'a`" is a type
+variable (the tick mark just indicates that the variable ranges over
+types rather than over values). "`Ï1 > Ï2`" is the type of a
+function from expressions of type `Ï1` to expressions of type `Ï2`.
+And "`â'a. Ï`" is called a universal type, since it universally
+quantifies over the type variable `'a`. (You can expect that in
+`â'a. Ï`, the type `Ï` will usually have at least one free occurrence
+of `'a` 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
calculus, except that they have their shrug variable annotated with a
type. Applications "`e1 e2`" are just like in the simplytyped lambda calculus.
+
In addition to variables, abstracts, and applications, we have two
additional ways of forming expressions: "`Î'a. e`" is a type
abstraction, and "`e [Ï]`" is a type application. The idea is that
Λ
is a capital λ
. Just like
the lowercase λ
, Λ
binds
variables in its body; unlike λ
,
Λ
binds type variables. So in the expression
+additional ways of forming expressions: "`Î'a. e`" is called a *type
+abstraction*, and "`e [Ï]`" is called a *type application*. The idea
+is that Λ
is a capital λ
: just
+like the lowercase λ
, Λ
binds
+variables in its body, except that unlike λ
,
+Λ
binds type variables instead of expression
+variables. So in the expression
Λ 'a (λ x:'a . x)
the Λ
binds the type variable `'a` that occurs in
the λ
abstract. This expression is a polymorphic
version of the identity function. It says that this one general
identity function can be adapted for use with expressions of any
type. In order to get it ready to apply to, say, a variable of type
boolean, just do this:
+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 to, say, a variable of type boolean, just do
+this:
(Λ 'a (λ x:'a . x)) [t]
The type application (where `t` is a type constant for Boolean truth
values) specifies the value of the type variable `α`, which is
the type of the variable bound in the `λ` expression. Not
+This type application (where `t` is a type constant for Boolean truth
+values) specifies the value of the type variable α, which is
+the type of the variable bound in the λ expression. Not
surprisingly, the type of this type application is a function from
Booleans to Booleans:
@@ 84,13 +90,16 @@ instantiated as a function from expresions of type `'a` to expressions
of type `'a`. In general, then, the type of the unapplied
(polymorphic) identity function is
(Λ 'a (λ x:'a . x)): (\forall 'a . 'a > 'a)


+(Λ 'a (λ x:'a . x)): (∀ 'a . 'a > 'a)
+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.
+[See Benjamin C. Pierce. 2002. *Types and Programming Languages*, MIT
+Press, pp. 350353, for `tail` for lists in System F.]
Types in OCaml

2.11.0