Computer Science Department
Programming Methods Laboratory

Theorie des Langages /
Fondements de la Programmation
Ecole Polytechnique Federale de Lausanne
Exercises 6

In our type reconstruction algorithm from the lecture, type reconstruction is done by solving a unification problem. Your task is to implement type unification according to Robinson's algorithm in Funnel.

Here's the abstract syntax of types:

    Type = TVar String
         | Arrow Type Type
         | TCon String {Type}
You should start with defining a visitor framework for types. Now try to find a good representation for substitutions. A substitution is a set of equations t == T where type variable t does not occur in type T.

Finally you should implement function mgu:

def mgu(T, T') s = ...
which takes two types T and T' and a substitution s and returns a new substitution s' so that
  • s' T == s' T', and
  • s' s = s'.