Exercise 10 Constraint Typing, Let-Polymorphism
English only
This page is preliminary and will be updated with the partial implementation on Wed 2005-12-01.

### 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 let-binding 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 22-2)
 ```unify( C ) ::= if empty( C ) then [] else let ::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(::::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 {}
(CT-Var)
 Γ |-F zero: Nat |F {}
(CT-Zero)
 Γ, x: T1 |-F t: T2 |H C Γ |-F \x: T1. t: T1 → T2 |H C
(CT-Abs)
 Γ |-F t: T |H C Γ |-F succ t: Nat |H C ∪ {T=Nat}
(CT-Succ)
 Γ |-F t1: T1 |H C1   Γ |-H t2: T2 |J C2 Γ |-X::F t1 t2: X |J C1 ∪ C2 ∪ { T1 = T2 → X }
(CT-App)
 Γ |-F t: T |H C Γ |-F pred t: Nat |H C ∪ {T=Nat}
(CT-Pred)
 Γ |-F t1: T1 |J C1   Γ, x:T |-J t2: T2 |K C2 Γ |-F let x: T1 = t1 in t2: T2 |K C1 C2
(CT-Let)
 Γ |-F t: T |H C Γ |-F isZero t: Bool |H C ∪ {T=Nat}
(CT-IsZero)
 Γ |-F t1: T1 |H C1 Γ |-H t2: T2 |J C2 Γ |-J t3: T3 |K C3 Γ |-F if t1 then t2 else t3: T2 |K C1 ∪ C2 ∪ C3
(CT-If)
 Γ |-F t: T |H C Γ |-F fix t: X |X::H C ∪ { T = X → X }
(CT-Fix)
 Γ, x: X |-F t: T |H C Γ |-X::F \x. t: X → T |H C
(CT-FreshAbs)
 Γ |-F t1: T1 |J C1 Γ, x:X |-J t2: T2 |K C2 Γ |-X::F let x = t1 in t2: T2 |K C1 C2
(CT-FreshLet)

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.

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.

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`?

Implement let - polymorphism: perform an evaluation step (term substitution) before type-checking 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?