Transcript Type Systems

Type Systems
Doaitse Swierstra
Atze Dijkstra
Components
lectures from the book “Types and
Programming Languages”, Benjamin
Pierce
study the type inferencer/checker of the
Utrecht Haskell Compiler (UHC)
project
small exercises
2
Prerequisites
Grammars and Parsing
Implementation of Programming
Languages
fluency in Haskell programming
3
Book
should be relatively easy to follow, but it
will take time (500 pages)
well written, with extensive set of
exercises
both theory and practice
uses ML as a demonstration and
implementation language
written at an easy pace
4
UHC
“extension” of IPT compiler
data types
multiparameter type classes
forall and existential quantifiers
polymorphic kinds
5
1. Modules
2. Extendible Records
Projects
3. Functional Dependencies
4. Typed AG
5. XMLambda
6. Unifying Kind and Type Inference
7. Kind Inferencing in Helium
8. Haskell Type System
9. Uniqueness Types
10.Implicit Arguments
6
1 Modules
import and export types
keep safety
class issues
parallel imports
typed annotations
ML functors
7
2 Extendible Records
allow cartesian products with labelled
fields
subtype relation
use class sytem to express constraints
many different proposals exits
8
3 Functional Dep’cies
allow parameters in instance definitions
to have a functional relationship
very useful in multi-parameter type
classes
implemented in Hugs and GHC
9
Typed AG
add elements of Haskell to AG system
delicate choice of features has to be
made
useful work, as you will all recognise
10
XMLambda
yet another approach to extendible
records
moves further away from Haskell
has nice applications
11
Unifying Type and Kind
Inference
type inference and kind inference are
very similar
make the code look just as similar
can this be extended to even more
levels?
12
Kind Inference in Helium
Helium: light weight Haskell for first year
students
excellent error messages
tranport kind inference to helium
contraint based type inferencer
13
Haskell Type System
study the full haskell type system
document missing features from UHC
add some of the still missing elements
14
Uniqueness Types
the type system keep tracks of the
number of references to a value (1 or
>1)
replacement for IO monad
invented and implemented in Clean
makes efficient implementation possible
avoids dynamic garbage collection
15
Implicit Arguments
generalise the class parameters
extend haskell so you can make
classes into first class citizens
16
What to do now?
if you want a specific partner then
choose a partner
decide on your preferences ranking 1-5
for your top 5 preferred projects
mail to [email protected] before
tomorrow 17.00
17
Chapter 1-10
motivation
mathematical preliminaries
untyped arithmetic expressions
the untyped lambda calculus
nameless representation of terms
18
1-10 continued
ML implementation
Typed arithmetic expressions
Simply typed lanbda calculus
ML implementation
19
Observations
nothing in these chapters should come
as a surpsise
and you should just browse/read
ML is used:
somewhat baroque notation!!
strict evaluation!!
the theory treated at some points
relies on this!, so keep this in mind
20
Why types?
originally: data organistation, layout of
data in memory: PIC (99)
overloading, nice notation: 3+5.0
programs should not go wrong
elementary operations are applied to
bit patterns that represent the kind of
data they expect
programs do terminate
21
Why Types?
assist in organisation of program code
dependent types => total correctness
a type system constrains the number of
legal programs is some useful way
22
Kind of Typing Systems
dynamic typing (LISP, Java coercions)
static typing (as you know it)
Higher Order Logic, Automath
integration with theorem provers
the type system can express every
property of a program
23
Proving program properties
operational semantics
big step semantics
small step semantics
denotational semantics
axiomatic semantics
Our preference here
Lambda calculus
we can express every possible
computation in the untyped lambda
calculus
25
Booleans
t ::= true
| false
| if t then t else t
v ::= true
| false
if true then t1 else t2 => t1
if false then t1 else t2 => t2
26
Booleans (strict evaluation)
note that the condition is evaluated
before the expressions themselves are
t1 -> t1’
if t1 then t2 else t3 =>
if t1’ then t2 else t3
27
Observe
evaluation is deterministic (i.e. always
exactly one rule applies)
evaluation always terminates
normal forms are unique
28
Arithmetic Expressions
t ::=
|
|
|
0
succ t
pred t
iszero t
nv :: = 0
|
succ nv
t1 => t2
succ t1 => succ t2
29
Booleans
tru = \t.\f.t
fls = \t.\f.f
if = \c.\t.\e. c t e
if tru 2 3
(\c.\t.\e. c
(
\t.\e. tru
(
\e. tru
tru
(\t.\f.t)
(
\f.2)
(
2)
=>
t e) tru 2 3 =>
t e)
2 3 =>
2 e)
3 =>
2 3
=>
2 3
=>
3
=>
30
Integers
c0
c1
c2
c3
=
=
=
=
\s.\z.
z
\s.\z.
s z
\s.\z.s
(s z)
\s.\z.s (s (s z))
31
Recursion!!
omega = (\x. x x)(\x. x x) ??
fix = \f.(\x. f(x x))
(\x. f(x x))
fix g
=>
(\x. g(x x))(\x. g(x x)) =>
g((\x. g(x x))(\x. g(x x))) =>
g (fix g)
32
Recursion (cont.)
note that fix generates copies of g if
necessary
and passes the generater on to this g
so that g can generate new copies is
necessary
33
Exercise
try to find a type for fix
if you cannot find one, try to explain why
you cannot
34
Untyped lambda calculus
v :: = \x.t
t ::= x
| \x.t
| t t
35
De Bruijn Indices
represent lambda terms without using
identifiers
an identifier is replaced by a number
indicating how far the argument is
removed from the top of the stack
36
Example
is represented by
37
Terms
38
Exercise
define a Haskell data type for the
untyped lambda calculus with variables
define a Haskell data type for
representing de Bruijn terms
define a translation from the first to the
second
write a small interpreter for the latter
39
Hint
Chapter 6: de Bruijn numbers
Chapter 7: an interpreter in ML
40