A library for constraint-based Hindley-Milner type inference
Library inferno
Module Inferno . Unifier . Make


module S : sig ... end


type variable

A unifier maintains a graph whose vertices are equivalence classes of variables. With each equivalence class, a piece of information of type data is attached.

type 'a structure = 'a S.structure

The type 'a structure describes the information that is attached with each class. It is parameterized over a type 'a of children. In the definition of the type data, 'a is instantiated with variable.

type data = variable structure

By definition, data is a synonym for variable structure. So, the data attached with an equivalence class of variables is a structure whose children are variables.

val get : variable -> data

get v is the structure currently attached with the (equivalence class of the) variable v. The structure that is attached with a class can change when the unifier is invoked.

exception Unify of variable * variable

This exception is raised by unify.

val unify : variable -> variable -> unit

unify v1 v2 equates the two variables v1 and v2. These variables become part of the same equivalence class. The structures carried by v1 and v2 are combined by invoking the conjunction function supplied by the user as an argument to Unifier.Make. conjunction itself is given access to an equate function which submits an equality constraint to the unifier.

If a logical inconsistency is detected, Unify (v1, v2) is raised, and the state of the unifier is unaffected. (The unifier undoes any updates that it may have performed.) For this undo machinery to work correctly, the conjunction function provided by the user must not perform any side effect.

Unification can create cycles in the graph maintained by the unifier. By default, the unifier tolerates these cycles. An occurs check, which detects these cycles, is provided separately: see OccursCheck.Make. Because cycles are permitted, the variables v1 and v2 carried by the exception Unify can participate in cycles. When reporting a unification error, a cyclic decoder should be used: see Decoder.Make.

val is_representative : variable -> bool

is_representative v determines whether the variable v is currently the representative element of its equivalence class.

val fresh : data -> variable

fresh s creates a new variable whose structure is s. This variable forms an equivalence class of its own.