Description
Question 1[25 points]
Crucial to the unification algorithm is the side condition α 6∈ FV(t) in the rules Inst 1 and
Inst 2. This condition is called occurs check, because we must check whether the variable
α occurs in the type t. In this question you are asked to implement the following function
for the occurs check.
occursCheck: (tp option) ref * tp -> unit
Given a type variable a and a type t, it will return unit if a does not occur in the type t.
Otherwise it will raise the exception OccursCheck.
Question 2[35 points]
In this question you are asked to implement a function unifiable which checks whether two
types are unifiable.
unifiable: tp * tp -> unit
The function expects two types t and s and will return unit if the two types are unifiable.
As a side-effect it will instantiate destructively all the free type variables occurring in t and
s. If two types t and s are not unifiable, it will raise an exception Error. Use the exception
Error to propagate error messages.
Question 3[20 points] Informally derive the type for the apply-list function defined below.
This function takes a list of functions and produces a single function which is the composite
of all of them. If the list is empty one gets the identity function.
The code is shown below.
fun apply_list [] = (fn x => x)
| apply_list(f::fs) = (fn x => apply_list(fs)(f(x)))
Question 4[20 points] Informally derive the type of the function foo below.
fun foo x = x:= (!x)+1.
2