inferno

A library for constraint-based Hindley-Milner type inference
Library inferno

Parameters

module S : sig ... end

Signature

Unification

module Data : sig ... end

This submodule defines the data attached with a unification variable.

module U : sig ... end

This unifier operates with the structure specified by the submodule Data.

type variable = U.variable

The variables manipulated by this module are unifier variables.

Schemes

type scheme

A scheme is usually described in the literature under the form ∀V.T, where V is a list of type variables (the quantifiers) and T is a type (the body).

Here, a scheme is represented as an abstract data structure. The functions quantifiers and body give a view of a scheme that matches the description in the literature.

Two key operations on schemes are generalization and instantiation. Generalization turns a fragment of the unification graph into a scheme. Instantiation operates in the reverse direction and creates a fresh copy of a scheme, which it turns into a graph fragment.

val quantifiers : scheme -> variable list

quantifiers σ returns the quantifiers of the scheme σ, in an arbitrary fixed order. The quantifiers are generic unifier variables. They carry no structure.

val body : scheme -> variable

body σ returns the body of the scheme σ. It is represented as a variable, that is, a vertex in the unification graph.

val trivial : variable -> scheme

trivial v creates a trivial scheme, whose list of quantifiers is empty, and whose body is v. A trivial scheme is also known as a monomorphic scheme. Nontrivial schemes are created by the functions enter and exit below.

Generalization and Instantiation

This module maintains a mutable internal state, which is created and initialized when Make is applied. This state is updated by the functions that follow: flexible, rigid, enter, exit, instantiate.

This internal state keeps track of a constraint context, which can be thought of as a stack of frames. The function enter pushes a new frame onto this stack; the function exit pops a frame off this stack (and performs generalization). enter is invoked when the left-hand side of a let constraint is entered; exit is invoked when it is exited. Thus, each stack frame corresponds to a surrounding let constraint. Every stack frame records the set of unifier variables that are bound there.

As unification makes progress, the site where a unifier variable is bound can change. Indeed, when two variables bound at two distinct stack frames are merged, the merged variable is thereafter considered bound at the most ancient of these stack frames.

val flexible : variable S.structure -> variable

flexible s creates a fresh unifier variable with structure s. This variable is flexible: this means that it can be unified with other variables without restrictions. This variable is initially bound at the most recent stack frame. If is unified with more ancient variables, then its binding site is implicitly hoisted up.

Invoking flexible is permitted only if the stack is currently nonempty, that is, if the current balance of calls to enter versus calls to exit is at least one.

val rigid : unit -> variable

rigid() creates a fresh unifier variable v with structure S.leaf. This variable is rigid: this means that it can be unified with a flexible variable that is as recent as v or more recent than v, and with nothing else. It cannot be unified with a more ancient flexible variable, with another rigid variable, or with a variable that carries nonleaf structure. This variable is bound at the most recent stack frame, and its binding site is never hoisted up.

By convention, at each stack frame, the rigid variables are bound in front of the flexible variables. Thus, a call to flexible and a call to rigid commute.

Invoking rigid is permitted only if the stack is currently nonempty, that is, if the current balance of calls to enter versus calls to exit is at least one.

val enter : unit -> unit

enter() updates the current state by pushing a new frame onto the current constraint context. It is invoked when the left-hand side of a CLet constraint is entered.

exception Cycle of variable

This exception is raised by exit.

exception VariableScopeEscape

This exception is raised by exit.

val exit : rectypes:bool -> variable list -> variable list * scheme list

exit ~rectypes roots updates the current state by popping a frame off the current constraint context. It is invoked when the left-hand side of a CLet constraint is exited.

exit examines the young fragment of the unification graph, that is, the part of the unification graph that has been created or affected since the most recent call to enter. The following actions are taken.

First, if rectypes is false, then an occurs check is performed: that is, if there is a cycle in the young fragment, then an exception of the form Cycle v is raised, where the vertex v participates in the cycle.

Second, every young unification variable is inspected so as to determine whether its logical binding site can be hoisted up to a strictly older frame or must remain part of the most recent frame. In the latter case, the variable is generalizable. A list vs of the generalizable variables is constructed. If a rigid variable is found to be non-generalizable, then VariableScopeEscape is raised.

Third, for each variable root provided by the user in the list roots, a scheme is constructed. The body of this scheme is the variable root. Its quantifiers are the structureless generalizable variables that are reachable from this root. They form a subset of vs. A list of schemes schemes, in correspondence with the list roots, is constructed.

It may be the case that some variables in the list vs appear in none of the quantifier lists of the constructed schemes. These variables are generalizable and unreachable from the roots. They are logically unconstrained.

The pair (vs, schemes) is returned.

val instantiate : scheme -> variable list * variable

instantiate sigma creates a fresh instance of the scheme sigma. The generic variables of the type scheme are replaced with fresh flexible variables, obtained by invoking flexible. The images of the scheme's quantifiers and body through this copy are returned. The order of the scheme's quantifiers, as determined by the function quantifiers, is preserved.