inferno-experimental/src/Generalization.mli

194 lines
9.0 KiB
OCaml
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

(******************************************************************************)
(* *)
(* Inferno *)
(* *)
(* François Pottier, Inria Paris *)
(* *)
(* Copyright Inria. All rights reserved. This file is distributed under the *)
(* terms of the MIT License, as described in the file LICENSE. *)
(* *)
(******************************************************************************)
open Signatures
(**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 {i schemes}, together with several
operations that allow constructing, inspecting, and instantiating
schemes. *)
module Make
(S : sig (** @inline *) include GSTRUCTURE_OPT end)
: sig
(** {2 Unification} *)
(**This submodule defines the data attached with a unification variable. *)
module Data : sig
(** @inline *)
include DSTRUCTURE
(**The type ['a structure] is richer (carries more information) than the
type ['a S.structure]. The function [project] witnesses this fact. It
drops the extra information and extracts the underlying user-defined
structure. *)
val project : 'a structure -> 'a S.structure
end
(**This unifier operates with the structure specified by the submodule
{!Data}. *)
module U : sig
(** @inline *)
include GUNIFIER with type 'a structure = 'a Data.structure
end
(**The variables manipulated by this module are unifier variables. *)
type variable =
U.variable
(** {2 Schemes} *)
(**A {i scheme} is usually described in the literature under the form [∀V.T],
where [V] is a list of type variables (the {i quantifiers}) and [T] is a
type (the {i 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 {i generalization} and {i 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. *)
type scheme
(**[quantifiers σ] returns the quantifiers of the scheme [σ], in an arbitrary
fixed order. The quantifiers are {i generic} unifier variables. They carry
no structure. *)
val quantifiers: scheme -> variable list
(**[body σ] returns the body of the scheme [σ]. It is represented as a
variable, that is, a vertex in the unification graph. *)
val body: scheme -> variable
(**[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. *)
val trivial: variable -> scheme
(** {2 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 {i constraint context}, which can be
thought of as a stack of {i 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 {i 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. *)
(**[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 flexible: variable S.structure -> 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 rigid: unit -> variable
(**[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. *)
val enter: unit -> unit
(**This exception is raised by {!exit}. *)
exception Cycle of variable
(**This exception is raised by {!exit}. *)
exception VariableScopeEscape
(**[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 {i 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 {i 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 exit: rectypes:bool -> variable list -> variable list * scheme list
(**[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. *)
val instantiate: scheme -> variable list * variable
(**/**)
(**[show_state()] displays a representation of the internal state on the
standard output channel. It is used for debugging only. *)
val show_state: unit -> unit
end