Provides functions for type unification and type substitution.Terminologies:
A type substitution list is a list of pairs (a,ty) where a is a string representing a type variable and ty is a type. When applied to a another type tx, it will substitute all occurences of a in tx with ty.
tv : Type -> string list
tv ty
It returns the list of all type variables occuring in ty. Duplicates are removed.
tySubst : (string * Type) list -> Type -> Type
tySubst subst ty
It applies the type substitution list subst to the type ty.
@@ : ((string * Type) list * (string * Type) list) -> (string * Type) list
s @@ t
Given two type substitution s and t, the operator @@ combines them in such a way that:tySubst (s @@ t) ty = tySubst t (tySubst s ty)In otherwords, when the subsitution s @@ t is applied to a type ty, the substitution s is applied first, then t.
mgu : Type -> Type -> (string * Type) list
mgu ty1 ty2
It produces a type substitution that will unifiy ty1 and ty2. That is, if s is the resulting substitution, we have:tySubst s ty1 = tySubst s ty2Moreover, s is (suposedly) the most general unifier of ty1 and ty2. Keep in mind that a pair of types like a and [a] cannot be unified.If no unifier can be found, an exception will be raised.
exception unificationFail of Type * Type
raise unificationFail (ty1,ty2)
The exception is raised when ty1 and ty2 cannot be unified.