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.

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

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

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