Library

Module

Module type

Parameter

Class

Class type

sectionYPositions = computeSectionYPositions($el), 10)" x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)">

On This Page

Legend:

Library

Module

Module type

Parameter

Class

Class type

Library

Module

Module type

Parameter

Class

Class type

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 ... end`

`module Data : sig ... end`

This submodule defines the data attached with a unification variable.

`type variable = U.variable`

The 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 -> 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.

`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.

On This Page