FoP Exercises 8 30-May-2002 School of Computer and Communication Sciences Programming Methods Laboratory (LAMP)

 Home Staff Research Publications Events Teaching   FoP     Overview     Schedule     Slides     Tutorial     Contact     Links Jobs

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

Types are implemented according to the visitor pattern. 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.

You should implement function `mgu`:

`  def mgu(T: Type, T': Type)(s: Subst): Subst = ... `

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

Finally, you should implement function `tp` which makes use of the allready defined function `mgu`:

`  def tp(env: Env, E: Tree, T: Type)(s: Subst): Subst = ...`

You can use the framework provided in Unify.fnl

 [an error occurred while processing this directive]