This module provides machinery to deal with Hindley-Milner polymorphism. It takes care of creating and instantiating schemes, and does so in an efficient way. It is parameterized with the structure S. On top of it, it adds its own structure, because it needs every unification variable to carry extra information related to generalization. Thus, it wraps the user-specified structure S in a richer structure Data, and sets up a unifier U that works with this data. It provides an abstract representation of Hindley-Milner schemes, together with several operations that allow constructing, inspecting, and instantiating schemes.
module S : sig ... endmodule Data : sig ... endThis submodule defines the data attached with a unification variable.
type variable = U.variableThe variables manipulated by this module are unifier variables.
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.
quantifiers σ returns the quantifiers of the scheme σ, in an arbitrary fixed order. The quantifiers are generic unifier variables. They carry no structure.
body σ returns the body of the scheme σ. It is represented as a variable, that is, a vertex in the unification graph.
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 -> variableflexible 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 -> variablerigid() 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.
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.
This exception is raised by exit.
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.
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.