|
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'.
|