This page is preliminary and will be updated with the partial implementation on Wed 20051201.
Exercise 10 Constraint Typing, Let Polymorphism
This exercises deals with type inference, and constraint typing.
In constrast to previous exercises, we allow the programmer to either
put type annotations or leave them away, and use type variables X.
Another, minor difference is that we add an explicit fixpoint operator
fix , and will not use let rec anymore.
Source Language

Values

E ::= x T ::= X
E E Num
\x.E Bool
\x: T.E T>T
true
false
zero
succ E
pred E
iszero E
fix E
if E then E else E
let x = E in E
let x: T = E in E


V ::= BV
NV
\x: T.E
BV ::= true
false
NV ::= zero
succ NV


Every abstraction and letbinding that is not annotated can be treated as if
it had a fresh type variable. The source program generates a set of
contraints, which have to be unified in order to obtain a well typed program.
This is expressed by the following typing rules.
These classes are provided for types (from Type.scala )
class Type { ... }
case class TyVar(name: String) extends Type { // X
var is: Type = null;
}
case class TyBool extends Type; // Bool
case class TyNum extends Type; // Num
case class TyFun(from: Type, to:Type) extends Type; // T > T
Unification
Here's the standard unification algorithm (Fig 222)
unify( C ) ::= if empty( C ) then [] else let <S,T>::C' = C in
if S == T then unify(C')
else if S == X and X ∉ FV(T) then unify([X/T]C') o [X/T]
else if T == X and X ∉ FV(S) then unify([X/S]C') o [X/S]
else if S == S1 > S2 and T == T1 > T2 then
unify(<S1,T1>::<S2,T2>::C')
else fail

Our implementation will follow techniques described nicely in Baader, Nipkow: "Term Rewriting and All That".
To use memory efficiently, we will never build up or apply substitutions, but rather
set the "is " reference. This is very efficient,
however requires that whenever we deal with a type variable, we need to check whether
is!=null and dereference if necessary.
Constraint Typing
Here are the constraint typing rules, in the form suggested by TAPL Exc. 22.3.9.
The judgment Γ _{F} t: T _{J} C means that inputs Γ, F, t to the algorithm
produce T, J and C, where
 Γ is the context
 F is an infinite supply of fresh names
 t is a term
 T is a type
 J is a suffix of F
 C is a set of constraints
If X is the next fresh variable X we can take, this is indicated by the notation X::F.
Type System 
x:T ∈ Γ  Γ _{F} x:T _{F} {} 
 (CTVar) 
  Γ _{F} zero: Nat _{F} {} 
 (CTZero) 

Γ, x: T_{1} _{F} t: T_{2} _{H} C  Γ _{F} \x: T_{1}. t: T_{1} → T_{2} _{H} C 
 (CTAbs) 
 Γ _{F} t: T _{H} C  Γ _{F} succ t: Nat _{H} C ∪ {T=Nat} 
 (CTSucc) 

Γ _{F} t_{1}: T_{1} _{H} C_{1} Γ _{H} t_{2}: T_{2} _{J} C_{2}  Γ _{X::F} t_{1} t_{2}: X _{J} C_{1} ∪ C_{2} ∪ { T_{1} = T_{2} → X } 
 (CTApp) 
 Γ _{F} t: T _{H} C  Γ _{F} pred t: Nat _{H} C ∪ {T=Nat} 
 (CTPred) 

Γ _{F} t_{1}: T_{1} _{J} C_{1} Γ, x:T _{J} t_{2}: T_{2} _{K} C_{2}  Γ _{F} let x: T_{1} = t_{1} in t_{2}: T_{2} _{K} C_{1} C_{2} 
 (CTLet) 
 Γ _{F} t: T _{H} C  Γ _{F} isZero t: Bool _{H} C ∪ {T=Nat} 
 (CTIsZero) 

Γ _{F} t_{1}: T_{1} _{H} C_{1}  Γ _{H} t_{2}: T_{2} _{J} C_{2}  Γ _{J} t_{3}: T_{3} _{K} C_{3}  Γ _{F} if t_{1} then t_{2} else t_{3}: T_{2} _{K} C_{1} ∪ C_{2} ∪ C_{3} 
 (CTIf) 

Γ _{F} t: T _{H} C  Γ _{F} fix t: X _{X::H} C ∪ { T = X → X } 
 (CTFix) 

Γ, x: X _{F} t: T _{H} C  Γ _{X::F} \x. t: X → T _{H} C 
 (CTFreshAbs) 

Γ _{F} t_{1}: T_{1} _{J} C_{1}  Γ, x:X _{J} t_{2}: T_{2} _{K} C_{2}  Γ _{X::F} let x = t_{1} in t_{2}: T_{2} _{K} C_{1} C_{2} 
 (CTFreshLet) 

Dowonload the partial implementation.
A fresh name is generated with SymbolSupply.fresh(t.pos); , where
t is some expression whose position can be used when reporting type errors.
Similarly, when you construct a type, use the functions Type.TyBool(t.pos) , where
t is some expression whose position can be used when reporting type errors.
Task 10.1
Implement the missing method unify1 in class Infer.scala (just translate the unify algorithm to Scala). Watch out: there are no substitutions built up, only side effects to be performed.
Task 10.2
Implement the missing method analyze in class Analyzer.scala according to
the specification given above.
Instead of creating constraints, call the unification algo directly via infer.unify(t1,t2)
Try it with files from the test directory. Why can one not typecheck double.lam ? breakCallByValue.lam ?
Task 10.3
Implement let  polymorphism: perform an evaluation step (term substitution) before typechecking the body of the let. Try it with double.lam
For expression substitution, you can use Expr.subst(s,Y,t) , which returns the expression [Y/t]s
Now double.lam should typecheck.
Careful: In this partial implementation, we use a Map[String,Type] instead of the Context class from before. Type checking
happens before de Bruijn indexing. Is is a good idea to use Expr.subst as is? What purpose does de Bruijn indexing serve? How can you fix the problem?
