Transcript Types and Programming Languages

Types and Programming Languages
Lecture 7
Simon Gay
Department of Computing Science
University of Glasgow
2006/07
Lambda Calculus with Types
We introduce function types: A  B is the type of functions with
a parameter of type A and a result of type B.
Types are defined by this grammar:
T ::= int
| bool
|TT
By convention,  associates to the right, so that
A  B  C means A  (B  C).
Example
2006/07
int  int  int
curried function of two arguments
(int  int)  int
function which is given a function
Types and Programming Languages Lecture 7 - Simon Gay
2
Typing Rules for Functions
To make it easier to define the typing rules, we will modify the
syntax so that a -abstraction explicitly specifies the type of its
parameter.
v ::= integer literal
| true | false
| x:T.e
e ::= v
|x
| e + e | e == e | e & e | if e then e else e
| ee
T ::= int
| bool
|TT
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
3
Typing Rules for Functions
The rules are similar to those in SFL, but simpler because we
have function types.
, x : T  e : U
(T-Abs)
  x:T.e : T  U
  e : T  U   e': T
(T-App)
  ee': U
We also need the typing rules for SEL, with environments added.
The resulting system is called the simply typed lambda calculus.
(A broad term: anything with T-Abs, T-App, and at least one
base type or ground type such as int or bool.)
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
4
Simply Typed Lambda Calculus
  true : bool
  false : bool
  v : int
if v is an integer literal
x : T 
(T-Var)
x:T
  e : int   f : int
(T-Plus)
  e  f : int
  e : bool   f : bool
(T-And)
  e & f : bool
  e : int   f : int
  c : bool   e : T   f : T
(T-Eq)
(T-If)
  e  f : bool
  if c then e else f : T
, x : T  e : U
(T-Abs)
  x:T.e : T  U
2006/07
  e : T  U   e': T
(T-App)
  ee': U
Types and Programming Languages Lecture 7 - Simon Gay
5
Examples
x : int, y : int  x : int x : int, y : int  y : int
T  Plus
x : int, y : int  x  y : int
T  Abs
x : int  y:int.x  y : int  int
T  Abs
 x:int.y:int.x  y : int  int  int
f : int  int  f : int  int f : int  int  2 : int
T  App
f : int  int  f 2 : int
T  Abs
 f:int  int. f 2 : (int  int )  int
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
6
Termination
If a typable closed term of the simply typed lambda calculus is
executed, it is guaranteed to terminate.
If  e:T then for some value v, e * v.
(See Pierce chapter 12 for a proof.)
This result is usually called strong normalization and it is true
no matter which reduction strategy is used.
It might seem surprising, because we know that recursion can
be expressed in the lambda calculus (and we have even seen a
non-terminating reduction sequence).
The answer is that any term containing xx is untypable.
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
7
xx is untypable
If xx were typable, with some type T, then there would be a
derivation of x:U  xx :T for some type U.
What would this derivation look like?
x : U  x: U x : U  x : U
T  App
x : U  xx : T
We can see that U must be of the form U  T
but this is not possible (unless we have recursive types, which
are coming later).
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
8
Recursion in simply typed lambda calculus
If we want to use the fixed point operator Y to express recursive
function definitions in the simply typed lambda calculus then we
must introduce it as a new kind of term with its own reduction
and typing rules. In fact we need a collection of Ys, one for each
type. To improve readability we’ll call them fix.
  fix T : ( T  T )  T
(T-Fix)
fix T T v  v(x:T.(fix T T v)x)
where x is not free in v
(R-Fix)
Exercise: why is R-Fix like this, instead of
fix T v  v(fix T v) ?
And why are we only interested in fix at function types?
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
9
Recursion in simply typed lambda calculus
Example
Given a recursive function definition:
f(x:int) = if x==0 then 1 else x*f(x-1)
we can rewrite it as a recursively-defined -abstraction:
f = x:int.if x==0 then 1 else x*f(x-1)
then abstract again on the function name:
f:intint.x:int.if x==0 then 1 else x*f(x-1)
this term has type (int  int)  (int  int) and we use the
appropriate fix to get the function:
fixint int (f :int  int.x :int.if x  0 then 1 else x * f(x -1))
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
10
Naming
The lambda calculus does not seem to give a direct way of
expressing programs in the SFL style: a sequence of named
function definitions followed by an expression.
But we do have a way of associating a term with a name:
-abstraction and function application.
Given the program
f(x:int):int = body-f
g(x:int):int = body-g
e
we can construct -terms F and G corresponding to f and g, then
form
((f:intint.g:intint.e)F)G
so that f and g can be used within e, and F and G are only written
once.
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
11
Naming
We prefer to work more directly with a programmer-friendly
syntax. The idea is to write
let f(x:int):int = body-f
g(x:int):int = body-g
in e
end
and we can define a typing rule for let:
  e : T , x : T  e': U
  let x  e in e' end : U
(T-Let)
Semantically we regard let x = e in e’ as an abbreviation for
(x:T.e’)e .
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
12
Let and Multiple Definitions
A let with several definitions can be regarded as an abbreviation:
let f(x:int):int = body-f
g(x:int):int = body-g
in e
end
let f(x:int):int = body-f
in let g(x:int):int = body-g
in e
end
end
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
13
Let and Recursive Definitions
We want to allow let definitions to be recursive, intending that
recursive function definitions will be translated into the equivalent
of fix expressions.
There’s a small issue: let allows us to define values as well as
functions, but we don’t want to allow recursively-defined values
(why not?)
A convenient solution is to distinguish between value and
function definitions by using the keywords val and fun.
let fun f(x:int):int = body-f
fun g(x:int):int = body-g
val a:int = 1
in e
end
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
14
Simply Typed Lambda Calculus is Safe
It is straightforward to prove type preservation and type safety
theorems for the simply typed lambda calculus, in the same way
as for the Simple Functional Language.
The same is true when we add recursion (using fix).
Exercise: prove type preservation and type safety theorems for
the simply typed lambda calculus.
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
15
A Better Functional Language
Combining the ideas so far (function types, let for introducing
names, fun and val to distinguish between function definitions
(can be recursive) and value definitions (can’t be recursive)),
introducing more convenient syntax for  (fn x:T => e instead
of x:T.e), and using = instead of is in function definitions,
we get a BFL.
BFL looks very much like a small subset of Standard ML.
Multi-argument functions must be curried.
An implementation of a typechecker for BFL can be found on
the course web page, together with a commentary.
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
16
Reading
Pierce: 9; 12 (more challenging) for the proof of termination.
Exercises
Pierce: 9.2.1, 9.2.2, 9.2.3, 9.3.9, 9.3.10, 9.4.10
2006/07
Types and Programming Languages Lecture 7 - Simon Gay
17