TypeLib

DATE : August 2001
AUTHOR : underdarkPrime
ADDRESS : underdarkPrime@yahoo.com

Index


  1. @@
  2. mgu
  3. tySubst
  4. unificationFail
  5. tv

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

tv : Type -> string list

tv ty



It returns the list of all type variables occuring in ty. Duplicates are removed.

tySubst

 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

 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 ty2
Moreover, 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.


unificationFail

 exception unificationFail of Type * Type 

 raise unificationFail (ty1,ty2)



The exception is raised when ty1 and ty2 cannot be unified.

Generated by mosmldoc --underdarkPrime