Compare commits

..

1 Commits

Author SHA1 Message Date
Olivier c2dfd17f68 Separate the status type in two. 2022-03-17 18:33:51 +01:00
26 changed files with 494 additions and 822 deletions

View File

@ -1,12 +1,6 @@
# Changes
## 2022/06/03
* Support for rigid variables, that is, variables that cannot be unified with
other rigid variables or with older flexible variables. These variables are
introduced by the new combinators `letr1` and `letrn`. The exception
`VariableScopeEscape`, which is raised when a rigid variable escapes its
scope, is also new.
## 2022/02/XX
* **Incompatible** changes to the solver's high-level API.
The module `Inferno.SolverHi` has been renamed to `Inferno.Solver`.

View File

@ -84,8 +84,7 @@ VERSIONS := \
4.10.0 \
4.11.1 \
4.12.0 \
4.13.1 \
4.14.0 \
4.13.0 \
.PHONY: versions
versions:
@ -118,7 +117,7 @@ DOC = $(DOCDIR)/inferno/index.html
doc:
@ rm -rf _build/default/_doc
@ dune clean
@ dune build @doc 2>&1 | ./doc.sh
@ dune build @doc
@ echo "You can view the documentation by typing 'make view'".
.PHONY: view

19
TODO.md
View File

@ -23,6 +23,15 @@
that would require multiple name transformations (i.e., composing multiple
environment lookups).
* Can `let0`, `let1`, and `letn` be simplified or combined? Do we really need
a `CLet` form that binds several names at once? Can the treatment of
unreachable type variables be simplified?
* Solving a `CLet` constraint produces a list of pairs `tevar * scheme`,
but `letn` keeps only the second component of every pair. If `letn`
is the only entry point, then the result type of `CLet` constraints
can be simplified.
* Can we remove the redundancy between `instance` and `instance_? (See next item.)
* Introduce a combinator `ignore : 'a co -> unit co` that allows the solver to
@ -33,12 +42,8 @@
elaboration. Also, it could remove the need for a primitive `instance_`
combinator, as `instance_ x ty` would correspond to `ignore (instance x ty)`.
* Introduce a `forall` combinator so as to make it easy to express `∀α.c`.
## Error Handling
* Attach exploitable information to the exception `VariableScopeEscape`.
* Introduce more powerful combinators to handle errors in a programmatic
way. Change the type `'a co` to `('a, 'b) co`? Introduce a `CCatch`
construct to allow recovering after an error? (Think about Merlin,
@ -60,6 +65,12 @@
decoding is performed either during elaboration or after the
unifier has encountered an error.
* Improve the documentation produced by `make doc`.
* Document the requirement that the function passed to `map` must be pure.
Use this hypothesis to remove the useless evaluation of `k1 env` in the
definition of `^^`.
## Test Suite
* Improve the coverage of the test suite. Add explicit negative test cases.

View File

@ -22,8 +22,8 @@ module O = struct
let inject n =
2 * n
type 'a structure = 'a S.structure
let pprint = S.pprint
type 'a structure =
'a S.structure
type ty =
F.nominal_type
@ -381,14 +381,12 @@ let hastype (typedecl_env : ML.datatype_env) (t : ML.term) (w : variable) : F.no
by t, but they can still be instantiated in the rest of the term.
*)
let x = X.fresh () in
let+ (alphas, (betas, _), t', tys) =
letr1 (List.length vs) x
(fun tys z ->
let tyvs = List.combine vs tys in
convert_annot typedecl_env tyvs z t ty)
let+ (alphas, t', tys) =
letr1 vs x
(fun tyvs z -> convert_annot typedecl_env tyvs z t ty)
(instance x w)
in
F.ftyapp (coerce alphas betas (F.ftyabs alphas t')) tys
F.ftyapp (F.ftyabs alphas t') tys
end
| ML.Tuple (pos, ts) ->
@ -616,7 +614,6 @@ type nonrec range = range
exception Unbound of range * ML.tevar
exception Unify = Solver.Unify
exception Cycle = Solver.Cycle
exception VariableScopeEscape = Solver.VariableScopeEscape
let hastype (env : ML.datatype_env) (t : ML.term) : F.nominal_term co =
let+ (vs, t) =

View File

@ -2,7 +2,6 @@ type range = Lexing.position * Lexing.position
exception Unbound of range * ML.tevar
exception Unify of range * F.nominal_type * F.nominal_type
exception Cycle of range * F.nominal_type
exception VariableScopeEscape of range
(* Contraint generation, constraint solving and elaboration, combined. *)
val translate: rectypes:bool -> ML.datatype_env -> ML.term -> F.nominal_term

View File

@ -62,20 +62,4 @@ rule read =
| "..." { DOTS }
| "#use" { USE }
| eof { EOF }
| "(*" { ocamlcomment lexbuf; read lexbuf }
| _ as c { failwith (Printf.sprintf "Unexpected character during lexing: %c" c) }
(* Skip comments. Comments can be nested. Note that we do not recognize
string or character literals inside comments. *)
and ocamlcomment = parse
| "*)"
{ () }
| "(*"
{ ocamlcomment lexbuf; ocamlcomment lexbuf }
| newline
{ next_line lexbuf; ocamlcomment lexbuf }
| eof
{ failwith "Unterminated OCaml comment." }
| _
{ ocamlcomment lexbuf }

View File

@ -67,10 +67,8 @@ let term :=
| ~ = term_abs ; <>
let term_abs :=
| FUN ; xs = list (tevar_) ; "->" ; t = term_abs ;
{
List.fold_right (fun x t -> Abs ($loc, x, t)) xs t
}
| FUN ; x = tevar_ ; "->" ; t = term_abs ;
{ Abs ($loc, x, t) }
| (x, t1, t2) = letin(tevar) ; { Let ($loc, x, t1, t2) }
@ -167,7 +165,6 @@ let type_atom :=
let type_annotation :=
| ty = typ; { (Flexible, [], ty) }
| SOME ; xs = list(tyvar) ; "." ; ty = typ ;
{ (Flexible, xs, ty) }
| FOR ; xs = list(tyvar) ; "." ; ty = typ ;

View File

@ -110,30 +110,6 @@ let print_let_in lhs rhs body =
^^ string "in"
^^ prefix 0 1 empty body
let rec flatten_tyabs t =
match t with
| TyAbs (x, t) ->
let (xs, t) = flatten_tyabs t in
(x::xs, t)
| t ->
([], t)
let rec flatten_abs t =
match t with
| Abs (p, t) ->
let (ps, t) = flatten_abs t in
(p::ps, t)
| t ->
([], t)
let print_nary_abstraction abs print_arg args rhs =
string abs
^^ space
^^ separate_map space print_arg args
^^ space
^^ string "->"
^//^ rhs
let print_annot print_elem (rigidity, tyvars, typ) =
let rigidity_kwd =
string @@ match rigidity with
@ -156,17 +132,21 @@ let rec print_term t =
and print_term_abs t =
group @@ match t with
| TyAbs _ ->
let (xs, t) = flatten_tyabs t in
print_nary_abstraction "FUN" print_tyvar xs (print_term_abs t)
| TyAbs (x, t1) ->
string "FUN" ^^ space
^^ print_tyvar x ^^ space
^^ string "->"
^//^ print_term_abs t1
| Let (p, t1, t2) ->
print_let_in
(print_pattern p)
(print_term t1)
(print_term_abs t2)
| Abs _ ->
let (ps, t) = flatten_abs t in
print_nary_abstraction "fun" print_pattern ps (print_term_abs t)
| Abs (p, t) ->
string "fun" ^^ space
^^ print_pattern p ^^ space
^^ string "->"
^//^ print_term_abs t
| t ->
print_term_app t

View File

@ -37,13 +37,6 @@ let translate ~verbose ~rectypes e t =
Printf.fprintf stdout "%!";
end;
None
| Infer.VariableScopeEscape range ->
if verbose then begin
Printf.fprintf stdout
"%sA rigid variable escapes its scope.\n%!"
(LexUtil.range range);
end;
None
let equal_term t1 t2 =
ML.compare_term t1 t2 = 0
@ -128,7 +121,7 @@ let test_with_args
(LexUtil.range range);
false
| t' ->
assert (equal_term t t');
assert (equal_term t t');
(* now we check typability; inference should not fail *)
let outcome_env =
ML2F.translate_env env in

View File

@ -1,2 +0,0 @@
type nat = | Zero | Succ of nat
let f = (fun x -> x : nat -> nat)

View File

@ -1,2 +0,0 @@
let g = fun f ->
(f : for 'a. 'a -> 'a)

View File

@ -1,4 +0,0 @@
(* We have a redundant quantifier here: 'b is not used in the type
annotation. *)
let _ =
(fun x -> x : for 'a 'b. 'a -> 'a) ()

View File

@ -1,4 +0,0 @@
(* We have unreachable generalizable variables inside the left-hand
side of a [letr] combinator. *)
let _ =
((fun x -> fun y -> y) (fun x -> x) : for 'a. 'a -> 'a) ()

View File

@ -103,8 +103,9 @@ Option type
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 a1 ->
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
FUN a0 ->
FUN a1 ->
Some<option {a1 -> a1*a0 -> a0}> (fun (x : a1) -> x, fun (x : a0) -> x)
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -178,20 +179,6 @@ List type
Converting the System F term to de Bruijn style...
Type-checking the System F term...
Annotations
$ cat nat-annot.midml
type nat = | Zero | Succ of nat
let f = (fun x -> x : nat -> nat)
$ midml nat-annot.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
(fun (x : nat ) -> x : nat -> nat )
Converting the System F term to de Bruijn style...
Type-checking the System F term...
Pattern-matching
$ cat match-tuple.midml
@ -222,11 +209,12 @@ Pattern-matching
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
FUN a0 a1 ->
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
| None<option (a1 -> a1)> () -> None<option a0> ()
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
end
FUN a0 ->
FUN a1 ->
match<option a0> Some<option (a1 -> a1)> (fun (x : a1) -> x) with
| None<option (a1 -> a1)> () -> None<option a0> ()
| (Some<option (a1 -> a1)> _ : option (a1 -> a1)) -> None<option a0> ()
end
Converting the System F term to de Bruijn style...
Type-checking the System F term...
@ -296,46 +284,6 @@ Here we see that the variable 'a is rigid inside the annotated term
(translated to a System F type abstraction), but can be used at any
instantiation type from the outside -- here the unit type {}.
This example is correct as well.
It involves a useless universal quantifier.
$ cat rigid-redundant.midml
(* We have a redundant quantifier here: 'b is not used in the type
annotation. *)
let _ =
(fun x -> x : for 'a 'b. 'a -> 'a) ()
$ midml rigid-redundant.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
(FUN a1 a2 -> (fun (x : a2) -> x : a2 -> a2)) [[a0] a0] [{}] ()
Converting the System F term to de Bruijn style...
Type-checking the System F term...
This example is also correct.
It involves unreachable generalizable type variables,
that is, type variables that are both unconstrained
and unreachable from the entry point of a type scheme.
$ cat rigid-unreachable.midml
(* We have unreachable generalizable variables inside the left-hand
side of a [letr] combinator. *)
let _ =
((fun x -> fun y -> y) (fun x -> x) : for 'a. 'a -> 'a) ()
$ midml rigid-unreachable.midml
Type inference and translation to System F...
Formatting the System F term...
Pretty-printing the System F term...
(FUN a1 a2 ->
((fun (x : a1 -> a1) (y : a2) -> y) (fun (x : a1) -> x) : a2 -> a2))
[[a0] a0]
[{}]
()
Converting the System F term to de Bruijn style...
Type-checking the System F term...
The example below is incorrect, it tries to unify two distinct rigid
variables.
@ -378,24 +326,8 @@ its binding scope.
$ midml rigid-level-escape-wrong.midml
Type inference and translation to System F...
File "test", line 2, characters 12-13:
A rigid variable escapes its scope.
The example below is incorrect, a rigid variable tries to escape
its binding scope. The escape is only noticed at generalization
time when adjusting levels.
$ cat rigid-level-escape-later-wrong.midml
let g = fun f ->
(f : for 'a. 'a -> 'a)
In the example above,* the type of f is "old" relative to the
rigid-introducing annotation, but we don't notice during the
unification itself which only touches the arrow type ->, not the rigid
variable 'a. The escape will be noticed at generalization time, when
adjusting the level of the type nodes below the arrow.
$ midml rigid-level-escape-later-wrong.midml
Type inference and translation to System F...
File "test", line 2, characters 2-24:
A rigid variable escapes its scope.
Type error: type mismatch.
Type error: mismatch between the type:
r2
and the type:
r8

66
doc.sh
View File

@ -1,66 +0,0 @@
#!/bin/bash
set -euo pipefail
shopt -s extglob
# This script helps make sense of the error messages produced by odoc.
# A list of missing modules.
missing=""
while read line
do
buffer="$line"
case "$line" in
File*client*:)
# A warning about the directory client/. Stop.
echo "Skipping all warnings about client/."
break
;;
File*:)
read line
buffer="$buffer$line"
case "$line" in
"Warning: Couldn't find the following modules:")
read line
# A warning that some modules could not be found.
# Accumulate the names of the missing modules.
missing="$missing $line"
;;
"Warning: Failed to lookup type unresolvedroot(Stdlib)"*)
# A warning about Stdlib. Skip.
echo "Skipping warnings about Stdlib."
;;
"Warning: While"*)
read line
buffer="$buffer$line"
case "$line" in
"Failed to lookup type unresolvedroot(Stdlib)"*)
# A multi-line warning about Stdlib. Skip.
echo "Skipping warnings about Stdlib."
;;
*)
# Another kind of warning. Echo.
echo "$buffer"
;;
esac
;;
*)
# Another kind of warning. Echo.
echo "$buffer"
;;
esac
;;
*)
echo "$buffer"
;;
esac
done
# Show the missing modules.
echo "Missing modules:"
echo "$missing" | sed -e 's/^ *//' | tr " " "\n" | sort | uniq

View File

@ -12,7 +12,7 @@
open Signatures
module Make
(S : DSTRUCTURE)
(S : OSTRUCTURE)
(U : MUNIFIER with type 'a structure := 'a S.structure)
(O : OUTPUT with type 'a structure := 'a S.structure)
= struct
@ -20,6 +20,28 @@ open U
(* -------------------------------------------------------------------------- *)
(* Decoding a variable. *)
(* The public function [decode_variable] decodes a variable, which must have
leaf structure. The decoded variable is determined by the unique identity
of the variable [v]. *)
let decode_variable (v : variable) : O.tyvar =
let data = U.get v in
assert (S.is_leaf data);
O.inject (S.id data)
(* The internal function [decode_id] decodes a variable. As above, this
variable must have leaf structure, and the decoded variable is determined
by the unique identity [id], which is already at hand. *)
(* [O.variable] is used to convert the result from [O.tyvar] to [O.ty]. *)
let decode_id (id : id) : O.ty =
O.variable (O.inject id)
(* -------------------------------------------------------------------------- *)
(* An acyclic decoder performs a bottom-up computation over an acyclic graph. *)
let new_acyclic_decoder () : variable -> O.ty =
@ -35,9 +57,14 @@ let new_acyclic_decoder () : variable -> O.ty =
try
Hashtbl.find visited id
with Not_found ->
let a = O.structure (S.map decode data) in
(* Because the graph is assumed to be acyclic, it is ok to update
the hash table only after the recursive call. *)
let a =
if S.is_leaf data then
decode_id id
else
O.structure (S.map decode data)
in
Hashtbl.add visited id a;
a
@ -174,33 +201,36 @@ let new_cyclic_decoder () : variable -> O.ty =
with Not_found ->
(* Otherwise, compute a decoded value [a] for this vertex. *)
let a =
if Hashtbl.mem table id then begin
(* We have just rediscovered this vertex via a back edge. Its
status may be [Active] or [Rediscovered]. We change it to
[Rediscovered], and stop the traversal. *)
Hashtbl.replace table id Rediscovered;
(* Decode this vertex as a (μ-bound) variable, identified by
its unique identity [id]. *)
O.variable (O.inject id)
end
else begin
(* This vertex is not being visited. Before the recursive
call, mark it as being visited. *)
Hashtbl.add table id Active;
(* Perform the recursive traversal. *)
let a = O.structure (S.map decode data) in
(* Mark this vertex as no longer being visited. If it was
recursively rediscovered during the recursive call,
introduce a μ binder. (It would be correct but noisy to
always introduce a μ binder.) *)
let status =
try Hashtbl.find table id with Not_found -> assert false
in
Hashtbl.remove table id;
match status with
| Active -> a
| Rediscovered -> O.mu (O.inject id) a
end
if S.is_leaf data then
(* There is no structure. *)
decode_id id
else
(* There is some structure. *)
if Hashtbl.mem table id then begin
(* We have just rediscovered this vertex via a back edge. Its
status may be [Active] or [Rediscovered]. We change it to
[Rediscovered], and stop the traversal. *)
Hashtbl.replace table id Rediscovered;
decode_id id
end
else begin
(* This vertex is not being visited. Before the recursive
call, mark it as being visited. *)
Hashtbl.add table id Active;
(* Perform the recursive traversal. *)
let a = O.structure (S.map decode data) in
(* Mark this vertex as no longer being visited. If it was
recursively rediscovered during the recursive call,
introduce a μ binder. (It would be correct but noisy to
always introduce a μ binder.) *)
let status =
try Hashtbl.find table id with Not_found -> assert false
in
Hashtbl.remove table id;
match status with
| Active -> a
| Rediscovered -> O.mu (O.inject id) a
end
in
(* If this vertex is isolated, store the decoded value [a] in the
memoization table [visited]. (It would be correct to never

View File

@ -11,29 +11,22 @@
open Signatures
(**This module performs decoding, which is the task of traversing the data
structure maintained by the unifier and transforming it into a data
(**This module offers performs decoding, which is the task of traversing the
data structure maintained by the unifier and transforming it into a data
representation selected by the user (typically, some form of tree). It is
parameterized by the term structure [S], by the unifier [U], and by the
data representation [O]. Read-only access to the unifier's data structure
suffices.
Two decoding algorithms are proposed: the {i acyclic decoder} does not
tolerate cycles, and produces ordinary trees; whereas the {i cyclic
decoder} can deal with cycles, and produces trees that contain μ
binders.
The cyclic decoder can produce μ binders and μ-bound type variables.
Neither decoder has specific support for printing ordinary (-bound)
type variables. In the eyes of the decoders, a type variable is just
a vertex that has no structure; it is up to the user-supplied function
[O.structure] to determine how such a vertex must be printed. *)
suffices. Two decoding algorithms are proposed: the {i acyclic decoder}
does not tolerate cycles, and produces ordinary trees; whereas the {i
cyclic decoder} can deal with cycles, and produces trees that contain μ
binders. *)
module Make
(S : sig (** @inline *) include DSTRUCTURE end)
(S : sig (** @inline *) include OSTRUCTURE end)
(U : sig (** @inline *) include MUNIFIER
with type 'a structure := 'a S.structure end)
(O : sig (** @inline *) include OUTPUT
with type 'a structure := 'a S.structure end)
: sig (** @inline *) include DECODER
with type variable := U.variable
and type tyvar := O.tyvar
and type ty := O.ty end

View File

@ -11,7 +11,7 @@
open Signatures
module Make (S : GSTRUCTURE_OPT) = struct
module Make (S : STRUCTURE_LEAF) = struct
(* -------------------------------------------------------------------------- *)
@ -53,6 +53,10 @@ let base_rank =
(* -------------------------------------------------------------------------- *)
(* Rigid variables have a fixed rank -- lowering their rank is an error --
and a fixed leaf structure -- unifying them with a non-leaf structure
is an error. *)
(* We want to be able to mark an equivalence class as either "active" or
"generic". The unifier works with active variables only; it never sees a
generic variable. Generic variables are used as part of the representation
@ -67,16 +71,25 @@ let base_rank =
(* An active variable is intended to become generic some day. A generic
variable never becomes active again. *)
(* An active variable is either flexible or generic. *)
type status = Rigid | Flexible | Generic
(* A rigid variable has a fixed rank -- lowering its rank is an error --
and a fixed leaf structure -- unifying it with a non-leaf structure
is an error. *)
type rigidity = Rigid_ | Flexible_
type status =
| Rigid
| Flexible
| Generic
let rigidity_of_status status =
match status with
| Generic ->
assert false
| Flexible ->
Flexible_
| Rigid ->
Rigid_
let status_of_rigidity rigidity =
match rigidity with
| Flexible_ ->
Flexible
| Rigid_ ->
Rigid
(* -------------------------------------------------------------------------- *)
@ -126,43 +139,19 @@ type 'a data = {
mutable mark: mark;
}
(* A printer (for debugging purposes). *)
let pprint elem data =
let open PPrint in
utf8format "@%d[%d]" data.id data.rank ^^
S.pprint elem data.structure
(* [status] and [mark] are currently not printed. *)
(* This exception is raised when a rigid variable escapes its scope, that is,
when it is unified with (or becomes a child of) a variable of lesser rank.
At present, this exception does not carry any data; we do not yet know how
to produce a good error message in this situation. *)
exception VariableScopeEscape
(* If [data.status] is flexible, then [adjust_rank data k] is equivalent
to [data.rank <- min k data.rank]. If [data.status] is rigid, then it
causes an error. Indeed, the rank of a rigid variable is fixed; it can
never decrease. *)
(* [adjust_rank data k] is equivalent to [data.rank <- min k data.rank]. *)
let adjust_rank (data : 'a data) (k : rank) =
assert (data.status <> Generic);
if k < data.rank then
if data.status = Flexible then
data.rank <- k
else
raise VariableScopeEscape
if k < data.rank then data.rank <- k
(* The module [Data] is meant to be an argument for [Unifier.Make]. *)
(* The module [Data] satisfies the signature [USTRUCTURE] required by the
functor [Unifier.Make]. *)
module Data = struct
type 'a structure =
'a data
let pprint = pprint
let id data =
data.id
@ -207,33 +196,34 @@ module Data = struct
let structure = S.conjunction equate data1.structure data2.structure in
(* The new rank is the minimum of the two ranks. *)
let rank = min data1.rank data2.rank in
(* If either variable is rigid, the conjunction is also rigid. However,
unification in the presence of rigid variables is subject to certain
restrictions. *)
let status : status =
match data1.status, data1.rank, data2.status, data2.rank with
| Generic, _, _, _
| _, _, Generic, _ ->
assert false
| Flexible, _, Flexible, _ ->
Flexible
| Rigid, _, Rigid, _ ->
(* One cannot unify two rigid variables. *)
raise InconsistentConjunction
| Rigid, rigid_rank, Flexible, _
| Flexible, _, Rigid, rigid_rank ->
(* One cannot lower the rank of a rigid variable. *)
if rank < rigid_rank then raise VariableScopeEscape;
(* One cannot assign some structure to a rigid variable. *)
if Option.is_some structure then raise InconsistentConjunction;
Rigid
let fail () = raise InconsistentConjunction in
(* If either variables is rigid, the conjunction is also rigid. *)
let status =
match rigidity_of_status data1.status,
rigidity_of_status data2.status with
| Flexible_, Flexible_ ->
Flexible
(* One cannot unify two rigid variables, *)
| Rigid_, Rigid_ ->
fail ()
(* ... or lower the rank of a rigid variable, *)
| Rigid_, Flexible_ ->
if (rank < data1.rank) then fail ();
(* ... or give it a non-leaf structure. *)
if not (S.is_leaf structure) then fail ();
Rigid
| Flexible_, Rigid_ ->
if (rank < data2.rank) then fail ();
(* ... or give it a non-leaf structure. *)
if not (S.is_leaf structure) then fail ();
Rigid
in
(* There is no need to preserve marks during unification. *)
let mark = dummy in
{ id; structure; rank; status; mark }
let is_leaf data =
Option.is_none data.structure
S.is_leaf data.structure
let project data =
data.structure
@ -331,17 +321,11 @@ let register v r =
(* When a fresh unification variable is created, it receives the current rank,
and it is immediately registered at this rank. *)
let flexible structure =
let fresh rigidity structure =
let r = state.young in
let status = Flexible in
let v = U.fresh (Data.make structure r status) in
register v r;
v
let rigid () =
let r = state.young in
let status = Rigid in
let v = U.fresh (Data.make None r status) in
if rigidity = Rigid_ then
assert (S.is_leaf structure);
let v = U.fresh (Data.make structure r (status_of_rigidity rigidity)) in
register v r;
v
@ -469,7 +453,7 @@ let discover_young_generation () =
discovering a variable [v] cannot improve the value of [k] that we are
pushing down).
In the presence of cycles, the upward propagation phase is incomplete, in the
In the presence of cycles, the upward propation phase is incomplete, in the
sense that it may compute ranks that are higher than necessary. For
instance, imagine a cycle at rank 2, such that every leaf that is reachable
from this cycle is at rank 1. Then, in principle, this cycle can be demoted
@ -692,7 +676,7 @@ let schemify (root : variable) : scheme =
let exit ~rectypes roots =
(* Because calls to [enter] and [exit] must be balanced, we must have: *)
assert (state.young >= base_rank);
assert (state.young >= 0);
(* Discover the young variables. *)
let generation = discover_young_generation() in
@ -743,15 +727,15 @@ let exit ~rectypes roots =
let instantiate { generics; quantifiers; root } =
(* Create a flexible copy [v'] of every generic variable [v]. At this point,
the variable [v'] carries no structure. Record the correspondence between
(* Create a flexible copy [v'] of every generic variable [v]. At this point, the
variable [v'] carries no structure. Record the correspondence between
[v] and [v'] in the mapping. *)
let mapping : variable array =
generics |> Array.mapi (fun i v ->
let data = get v in
assert (data.status = Generic);
data.mark <- i;
flexible None
fresh Flexible_ S.leaf
)
in

View File

@ -22,7 +22,7 @@ open Signatures
operations that allow constructing, inspecting, and instantiating
schemes. *)
module Make
(S : sig (** @inline *) include GSTRUCTURE_OPT end)
(S : sig (** @inline *) include STRUCTURE_LEAF end)
: sig
(** {2 Unification} *)
@ -31,7 +31,7 @@ module Make
module Data : sig
(** @inline *)
include DSTRUCTURE
include OSTRUCTURE
(**The type ['a structure] is richer (carries more information) than the
type ['a S.structure]. The function [project] witnesses this fact. It
@ -52,6 +52,31 @@ module Make
type variable =
U.variable
(* Existentially-bound variables can "move" in the constraint: some
constraint-solving steps have the effect of hoisting their
existential quantifier out, to scope over a larger part of the
constraint -- this corresponds to lowering the rank of the
variable. They can also be unified with some structure. *)
(* We also support "rigidly-bound" variables that are not allowed to
move to a different binding place, or to unify with anything else
than themselves. This models language features with abstract
variables/types that cannot escape their scope, such as local
abstract types or existential unpacking. *)
type status = Rigid | Flexible | Generic
type rigidity = Rigid_ | Flexible_
(* The literature defines a type scheme as a type (the ``body''), placed in
the scope of a list of universal quantifiers. Here, the quantifiers are
just variables (which definitely carry no structure), while the body is
just a variable too (which possibly/probably carries some structure).
One may think of a type scheme as a fragment of the unification graph,
part of which is marked ``generic'' and is meant to be copied when the
type scheme is instantiated, part of which is not (the free variables, so
to speak). *)
(** {2 Schemes} *)
(**A {i scheme} is usually described in the literature under the form [∀V.T],
@ -87,8 +112,7 @@ module Make
(**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}.
functions that follow: {!fresh}, {!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
@ -104,33 +128,12 @@ module Make
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
(**[fresh ~rigidity s] creates a fresh unifier variable with structure [s].
This variable is initially bound at the most recent stack frame. Invoking
{!fresh} 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 fresh: rigidity -> variable S.structure -> 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
@ -140,27 +143,23 @@ module Make
(**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,
[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
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
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.
generalizable variables is constructed.
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].
@ -177,10 +176,10 @@ module Make
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
generic variables of the type scheme are replaced with fresh variables,
obtained by invoking {!fresh}. 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

View File

@ -12,7 +12,7 @@
open Signatures
module Make
(S : OSTRUCTURE)
(S : OCSTRUCTURE)
(U : MUNIFIER with type 'a structure = 'a S.structure)
= struct

View File

@ -16,7 +16,7 @@ open Signatures
parameterized by the term structure [S] and by the unifier [U]. Read-only
access to the unifier's data structure suffices. *)
module Make
(S : sig (** @inline *) include OSTRUCTURE end)
(S : sig (** @inline *) include OCSTRUCTURE end)
(U : sig (** @inline *) include MUNIFIER
with type 'a structure = 'a S.structure end)
: sig (** @inline *) include OCCURS_CHECK

View File

@ -28,9 +28,9 @@ type id = int
(* -------------------------------------------------------------------------- *)
(* [STRUCTURE] describes just the type ['a structure]. *)
(* [SSTRUCTURE] describes just the type ['a structure]. *)
module type STRUCTURE = sig
module type SSTRUCTURE = sig
(**A structure is a piece of information that the unifier attaches to a
variable (or, more accurately, to an equivalence class of variables).
@ -53,23 +53,14 @@ module type STRUCTURE = sig
which indicates the presence of an equality constraint. *)
type 'a structure
(**[pprint] is a structure printer, parameterized over a child printer.
It is used for debugging purposes only. *)
val pprint: ('a -> PPrint.document) -> 'a structure -> PPrint.document
end
(* -------------------------------------------------------------------------- *)
(* [USTRUCTURE] describes an input of [Unifier.Make]. *)
(* The following signatures enrich [STRUCTURE] with additional operations. *)
(* [CONJUNCTIBLE] describes structures with a [conjunction] operation,
as required by [Unifier.Make]. *)
module type CONJUNCTIBLE = sig
module type USTRUCTURE = sig
(** @inline *)
include STRUCTURE
include SSTRUCTURE
(**[InconsistentConjunction] is raised by {!conjunction}. *)
exception InconsistentConjunction
@ -100,23 +91,47 @@ module type CONJUNCTIBLE = sig
end
(* [IDENTIFIABLE] describes a structure with unique identifiers,
as required by [OccursCheck.Make] and [Decoder.Make]. *)
module type IDENTIFIABLE = sig
(* [OCSTRUCTURE] describes an input of [OccursCheck.Make]. *)
module type OCSTRUCTURE = sig
(** @inline *)
include STRUCTURE
include SSTRUCTURE
(**[iter] applies an action to every child of a structure. *)
val iter: ('a -> unit) -> 'a structure -> unit
(**[id] extracts the unique identifier of a structure. *)
val id: 'a structure -> id
end
(* [MAPPABLE] describes traversable, mappable structures. *)
module type MAPPABLE = sig
(* [OSTRUCTURE] describes an input of [Decoder.Make]. *)
module type OSTRUCTURE = sig
(** @inline *)
include STRUCTURE
include OCSTRUCTURE
(**[map] applies a transformation to the children of a structure,
while preserving the shape of the structure. *)
val map: ('a -> 'b) -> 'a structure -> 'b structure
(**[is_leaf s] determines whether the structure [s] is a leaf, that is,
whether it represents the absence of a logical constraint. This function
is typically used by a decoder to determine which equivalence classes
should be translated to "type variables" in a decoded type. *)
val is_leaf: 'a structure -> bool
end
(* [GSTRUCTURE] describes an input of [Structure.Option],
and also describes part of its output. *)
module type GSTRUCTURE = sig
(** @inline *)
include USTRUCTURE
(**[iter] applies an action to every child of a structure. *)
val iter: ('a -> unit) -> 'a structure -> unit
@ -131,74 +146,37 @@ module type MAPPABLE = sig
end
(* -------------------------------------------------------------------------- *)
(* [USTRUCTURE] describes an input of [Unifier.Make]. *)
module type USTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include CONJUNCTIBLE with type 'a structure := 'a structure
end
(* [OSTRUCTURE] describes an input of [OccursCheck.Make]. *)
module type OSTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include MAPPABLE with type 'a structure := 'a structure
(** @inline *)
include IDENTIFIABLE with type 'a structure := 'a structure
end
(* [DSTRUCTURE] describes an input of [Decoder.Make]. *)
module type DSTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include MAPPABLE with type 'a structure := 'a structure
(** @inline *)
include IDENTIFIABLE with type 'a structure := 'a structure
end
(* [GSTRUCTURE] describes an input of [Structure.Option]
and an input of [Solver.Make]. *)
module type GSTRUCTURE = sig
(** @inline *)
include STRUCTURE
(** @inline *)
include CONJUNCTIBLE with type 'a structure := 'a structure
(** @inline *)
include MAPPABLE with type 'a structure := 'a structure
end
(* [GSTRUCTURE_OPT] describes the output of [Structure.Option] and
(* [STRUCTURE_LEAF] describes the output of [Structure.Option] and
an input of [Generalization.Make]. *)
module type GSTRUCTURE_OPT = sig
module S : GSTRUCTURE
module type STRUCTURE_LEAF = sig
(** @inline *)
include GSTRUCTURE with type 'a structure = 'a S.structure option
include GSTRUCTURE
(**The constant [leaf] is a structure that represents the absence of a
logical constraint. It is typically used when a variable is created
fresh. *)
val leaf: 'a structure
(**[is_leaf s] determines whether the structure [s] is a leaf, that is,
whether it represents the absence of a logical constraint. This function
is typically used by a decoder to determine which equivalence classes
should be translated to "type variables" in a decoded type. *)
val is_leaf: 'a structure -> bool
end
(* [HSTRUCTURE] describes an input of [Solver.Make]. *)
module type HSTRUCTURE = sig
(** @inline *)
include GSTRUCTURE
(**[pprint] is a structure printer, parameterized over a child printer.
It is used for debugging purposes only. *)
val pprint: ('a -> PPrint.document) -> 'a structure -> PPrint.document
end
@ -321,7 +299,7 @@ end
module type OUTPUT = sig
(** @inline *)
include STRUCTURE
include SSTRUCTURE
(**A representation of decoded type variables. *)
type tyvar
@ -355,8 +333,12 @@ end
module type DECODER = sig
type variable
type tyvar
type ty
(**[decode_variable v] decodes the variable [v]. *)
val decode_variable: variable -> tyvar
(**[new_acyclic_decoder()] initiates a new decoding phase. It returns a
decoding function [decode], which can be used as many as times as one
wishes. Decoding requires the graph to be acyclic: it is a bottom-up

View File

@ -13,7 +13,7 @@ open Signatures
module Make
(X : TEVAR)
(S : GSTRUCTURE)
(S : HSTRUCTURE)
(O : OUTPUT with type 'a structure = 'a S.structure)
= struct
@ -24,9 +24,6 @@ module Make
type tevar =
X.t
type tevars =
tevar list
module TeVarMap =
Hashtbl.Make(X)
@ -38,9 +35,6 @@ module TeVarMap =
type variable =
int
type variables =
variable list
let fresh : unit -> variable =
Utils.gensym()
@ -56,17 +50,8 @@ type range =
type shallow_ty =
variable O.structure
type tyvars =
O.tyvar list
type tys =
O.ty list
type scheme =
tyvars * O.ty
type schemes =
scheme list
O.tyvar list * O.ty
(**A constraint of type ['a co] is a constraint whose resolution, if
successful, produces a value of type ['a]. The ability for the
@ -110,7 +95,7 @@ type _ co =
a decoded type which represents the value assigned to the
type variable [v] at the end of the resolution process. *)
| CInstance : tevar * variable -> tys co
| CInstance : tevar * variable -> O.ty list co
(**An instantiation constraint [CInstance (x, v)] requires the type
variable [v] to be an instance of the type scheme denoted by the
term variable [x]. Its result is a list of types that indicates
@ -121,27 +106,25 @@ type _ co =
the trivial (monomorphic) type scheme [v] in the constraint [c]. *)
| CLet :
variables * tevars * variables * 'a co * 'b co ->
(tyvars * schemes * 'a * 'b) co
(**The constraint [CLet rs xs vs c1 c2] is solved as follows:
- First, the constraint [rs.vs.c1] is solved.
- Then, for each pair [(x, v)] drawn from the lists [xs] and [vs]
(which must have the same length), the term variable [x] is
bound to the constraint abstraction [λv.rs.(vs\v).c1].
- Finally, under these bindings, the constraint [c2] is solved.
variable list * (tevar * variable) list * 'a co * 'b co ->
(O.tyvar list * (tevar * scheme) list * 'a * 'b) co
(**[CLet rs (List.combine xs vs) c1 c2] first constructs a list
[cs] of constraint abstractions by abstracting the type
variables [vs] in the constraint [c1], under the scope of the
rigid variables [rs]. Then, it binds the term variables [xs] to
the constraint abstractions [cs] in the constraint [c2].
Thus, the variables [rs] are initially regarded as rigid while [c1]
is solved and simplified; but, once this is done, their rigid
nature disappears and they become flexible before generalization
is performed. The scheme associated with the term variable [x]
has the corresponding type variable [v] as its root.
The semantic value of this constraint is a tuple of:
- a list [γs] of decoded type variables that may appear in the semantic
value [v1].
- a list of decoded schemes, in correspondence with the list [xs].
- the semantic value [v1] of the constraint [c1].
- the semantic value [v2] of the constraint [c2]. *)
It produces a tuple of 4 results, namely:
- a list [ws] of (decoded) type variables that may appear in [a1], hence
should be universally bound by the client in [a1]. In a typical
scenario, [a1] is a System F term, and the client must build a type
abstraction [\Lambda vs.a1]. Note that [ws] must contain at least
the (decodings of) the rigid variables [rs].
- an association list that maps each term variable in [xs] to the type
scheme that has been assigned to it while solving [c2].
- the value [a1] produced by solving the constraint [c1].
- the value [a2] produced by solving the constraint [c2].
*)
(* -------------------------------------------------------------------------- *)
(* Exceptions. *)
@ -149,7 +132,6 @@ type _ co =
exception Unbound of range * tevar
exception Unify of range * O.ty * O.ty
exception Cycle of range * O.ty
exception VariableScopeEscape of range
(* A pretty-printer for constraints, used while debugging. *)
@ -202,9 +184,7 @@ module Printer = struct
annot (x, v) ^^
string " in" ^/^
self c
| CLet (rs, xs, vs, c1, c2) ->
assert (List.length xs = List.length vs);
let xvs = List.combine xs vs in
| CLet (rs, xvs, c1, c2) ->
string "let" ^^
(if rs = [] then empty else brackets (separate_map space var rs)) ^^
separate_map (string " and ") annot xvs ^^
@ -280,8 +260,8 @@ module U = G.U
(* -------------------------------------------------------------------------- *)
(* The solver carries an environment, an immutable mapping of term variables
to type schemes. *)
(* The solver carries an environment, an immutable mapping of term
variables to type schemes. *)
module Env = struct
@ -305,11 +285,11 @@ end (* Env *)
(* -------------------------------------------------------------------------- *)
(* The solver maintains a mutable mapping of immutable type variables to
unifier variables. *)
(* We maintain a mutable mapping of immutable type variables to unifier
variables. *)
(* [uvar] looks up the mapping. [flexible] and [rigid] create a new unifier
variable and extend the mapping. [uunbind] removes a mapping. *)
(* [uvar] looks up the mapping. [ubind] creates a new unifier variable and
extends the mapping. [unbind] removes the mapping created by [bind]. *)
module UVar = struct
@ -323,15 +303,9 @@ module UVar = struct
(* This should never happen. *)
Printf.ksprintf failwith "Unbound variable %d" v
let flexible (v : variable) so =
let ubind (v : variable) status so =
assert (not (VarTable.mem table v));
let uv = G.flexible (OS.map uvar so) in
VarTable.add table v uv;
uv
let rigid (v : variable) =
assert (not (VarTable.mem table v));
let uv = G.rigid() in
let uv = G.fresh status (OS.map uvar so) in
VarTable.add table v uv;
uv
@ -357,41 +331,17 @@ end (* UVar *)
(in the acyclic case), regardless of how many calls to the decoder are
performed. *)
(* [decode_variable] decodes a variable, which must have
leaf structure. The decoded variable is determined by the unique identity
of the variable [v]. *)
let decode_variable (v : U.variable) : O.tyvar =
let data = U.get v in
match G.Data.project data with
| Some _ -> assert false
| None -> O.inject (G.Data.id data)
(* TODO explain *)
(* The module [D] is used to decode non-leaf structures *)
module D =
Decoder.Make (G.Data) (U) (struct
include O
let pprint = G.Data.pprint
let structure (s : O.ty U.structure) : O.ty =
match G.Data.project s with
| None -> O.variable (O.inject (G.Data.id s))
| Some s -> O.structure s
O.structure (OS.project_nonleaf (G.Data.project s))
end)
(* -------------------------------------------------------------------------- *)
(* Initialize a decoder for use during elaboration. If [rectypes] is on, a
cyclic decoder is used; otherwise, an acyclic decoder is used. *)
let decode : U.variable -> O.ty =
if rectypes then D.new_cyclic_decoder() else D.new_acyclic_decoder()
let decode_scheme (s : G.scheme) : scheme =
List.map decode_variable (G.quantifiers s),
decode (G.body s)
(* -------------------------------------------------------------------------- *)
(* The exceptions [Unify] and [Cycle], raised by the unifier, must be caught
and re-raised in a slightly different format.
@ -401,22 +351,28 @@ let decode_scheme (s : G.scheme) : scheme =
let unify range v1 v2 =
try
U.unify v1 v2
with
| U.Unify (v1, v2) ->
let decode = D.new_cyclic_decoder() in
raise (Unify (range, decode v1, decode v2))
| G.VariableScopeEscape ->
raise (VariableScopeEscape range)
with U.Unify (v1, v2) ->
let decode = D.new_cyclic_decoder() in
raise (Unify (range, decode v1, decode v2))
let exit range ~rectypes vs =
try
G.exit ~rectypes vs
with
| G.Cycle v ->
let decode = D.new_cyclic_decoder() in
raise (Cycle (range, decode v))
| G.VariableScopeEscape ->
raise (VariableScopeEscape range)
with G.Cycle v ->
let decode = D.new_cyclic_decoder() in
raise (Cycle (range, decode v))
(* -------------------------------------------------------------------------- *)
(* Initialize a decoder for use during elaboration. If [rectypes] is on, a
cyclic decoder is used; otherwise, an acyclic decoder is used. *)
let decode : U.variable -> O.ty =
if rectypes then D.new_cyclic_decoder() else D.new_acyclic_decoder()
let decode_scheme (s : G.scheme) : scheme =
List.map D.decode_variable (G.quantifiers s),
decode (G.body s)
(* -------------------------------------------------------------------------- *)
@ -439,7 +395,7 @@ let rec ok : type a . a co -> bool =
true
| CMap (c, _) ->
ok c
| CLet (_rs, _xs, _vs, _c1, c2) ->
| CLet (_rs, _xvs, _c1, c2) ->
(* The left-hand constraint [c1] does not need to be [ok], since it is
examined after a call to [G.enter]. *)
ok c2
@ -510,7 +466,7 @@ let rec solve : type a . range -> a co -> a on_sol =
unify range (uvar v) (uvar w);
On_sol (fun () -> ())
| CExist (v, s, c) ->
ignore (flexible v s);
ignore (ubind v G.Flexible_ s);
let result = solve range c in
uunbind v;
result
@ -531,16 +487,16 @@ let rec solve : type a . range -> a co -> a on_sol =
let a = solve range c in
Env.unbind x;
a
| CLet (rs, xs, vs, c1, c2) ->
| CLet (rs, xvs, c1, c2) ->
(* Warn the generalization engine that we are entering the left-hand
side of a [let] construct. *)
G.enter();
(* Register the rigid prefix [rs] with the generalization engine. *)
let urs = List.map (fun v -> rigid v) rs in
(* Register the rigid prefix [rs] with th generalization engine. *)
let _ = List.map (fun v -> ubind v G.Rigid_ None) rs in
(* Register the variables [vs] with the generalization engine, just as
if they were existentially bound in [c1]. This is what they are,
basically, but they also serve as named entry points. *)
let uvs = List.map (fun v -> flexible v None) vs in
let vs = List.map (fun (_, v) -> ubind v G.Flexible_ None) xvs in
(* Solve the constraint [c1]. *)
let (On_sol r1) = solve range c1 in
(* Ask the generalization engine to perform an occurs check, to adjust
@ -548,24 +504,25 @@ let rec solve : type a . range -> a co -> a on_sol =
of the type variables that were registered since the call to
[G.enter] above), and to construct a list [ss] of type schemes for
our entry points. The generalization engine also produces a list
[gammas] of the young variables that should be universally
[generalizable] of the young variables that should be universally
quantified here. *)
let gammas, ss = exit range ~rectypes uvs in
(* All rigid variables of [rs] must be generalizable. This assertion
may be costly and should be removed or disabled in the future. *)
assert (urs |> List.for_all (fun r -> List.mem r gammas));
List.iter uunbind vs;
(* Extend the environment [env]. *)
List.iter2 Env.bind xs ss;
let generalizable, ss = exit range ~rectypes vs in
List.iter (fun (_, v) -> uunbind v) xvs;
(* Extend the environment [env] and compute the type schemes [xss]. *)
let xss =
List.fold_right2 (fun (x, _) s xss ->
Env.bind x s;
(x, s) :: xss
) xvs ss []
in
(* Proceed to solve [c2] in the extended environment. *)
let (On_sol r2) = solve range c2 in
List.iter Env.unbind xs;
List.iter (fun (x, _) -> Env.unbind x) xss;
On_sol (fun () ->
List.map decode_variable gammas,
List.map decode_scheme ss,
r1(),
r2()
)
List.map D.decode_variable generalizable,
List.map (fun (x, s) -> (x, decode_scheme s)) xss,
r1 (),
r2 ())
(* The solver's state is now ready. The following function (which must be
called at most once, as it affects the solver's state) combines solving
@ -749,55 +706,73 @@ let single xs =
| _ ->
assert false
(* [letrn] is our most general combinator. It offers full access to the
expressiveness of [CLet] constraints. *)
let letrn
: 'client_tyvar list
-> tevar list
-> (('client_tyvar * variable) list
-> (tevar * variable) list
-> 'a co)
-> 'b co
-> (O.tyvar list * (tevar * scheme) list * 'a * 'b) co
= fun alphas xs f1 c2 ->
let rs = List.map (fun _a -> fresh ()) alphas in
(* The integer parameter [k] indicates how many rigid variables the user
wishes to create. These variables are rigid while the left-hand constraint
is solved. Once generalization has taken place, they become generic
variables in the newly-created schemes. *)
(* For each term variable [x], create a fresh type variable [v], as in
[CExist]. *)
let xvs = List.map (fun x ->
x, fresh ()
) xs in
let c1 = f1 (List.combine alphas rs) xvs in
let+ (generalizable, ss, v1, v2) =
CLet (rs, xvs, c1, c2)
in
(generalizable, ss, v1, v2)
(* [letr1] is a special case of [letrn], where only one term variable
is bound. *)
let letr1
: 'client_tyvar list
-> tevar
-> (('client_tyvar * variable) list -> variable -> 'a co)
-> 'b co
-> (O.tyvar list * 'a * 'b) co
= fun alphas x f1 c2 ->
let+ (generalizable, _ss, v1, v2) =
letrn alphas [x]
(fun rzs xzs ->
let (_,z) = single xzs in
f1 rzs z)
c2
in
(generalizable, v1, v2)
(* The general form of [CLet] involves two constraints, the left-hand side and
the right-hand side, yet it defines a *family* of constraint abstractions,
which become bound to the term variables [xs]. *)
let letrn k xs f1 c2 =
(* Allocate a list [rs] of [k] fresh type variables. *)
let rs = List.init k (fun _ -> fresh()) in
(* Allocate a fresh type variable for each term variable in [xs]. *)
let vs = List.map (fun _ -> fresh()) xs in
(* Apply [f1] to the lists [rs] and [vs], to obtain a constraint [c1]. *)
let c1 = f1 rs vs in
(* Done. *)
CLet (rs, xs, vs, c1, c2)
(* [letr1] is a special case of [letrn] where only one term variable
is bound, so the lists [xs], [vs], [ss] are singletons. *)
let letr1 k x f1 c2 =
let+ gammas, ss, v1, v2 = letrn k [x] (fun rs vs -> f1 rs (single vs)) c2
in gammas, single ss, v1, v2
(* [letn] is a special case of [letrn] where [k] is zero, so no rigid
variables are created. *)
let letn xs f1 c2 =
letrn 0 xs (fun _rs vs -> f1 vs) c2
let+ (generalizable, xss, s1, s2) =
letrn [] xs (fun _ xvs -> f1 (List.map snd xvs)) c2 in
let ss = List.map snd xss in
(generalizable, ss, s1, s2)
(* [let1] is a special case of [letn] where only one term variable
is bound, so the lists [xs], [vs], [ss] are singletons. *)
(* [let1] is a special case of [letn], where only one term variable is bound. *)
let let1 x f1 c2 =
let+ gammas, ss, v1, v2 = letn [x] (fun vs -> f1 (single vs)) c2
in gammas, single ss, v1, v2
let+ (generalizable, ss, v1, v2) =
letn [ x ] (fun vs -> f1 (single vs)) c2
in (generalizable, single ss, v1, v2)
(* [let0] is a special case of [letn], where no term variable is bound, and
the right-hand side is [CTrue]. The constraint produced by [let0] is [ok]
by construction; in other words, it is a suitable argument to [solve]. *)
let let0 c1 =
let+ gammas, _, v1, () = letn [] (fun _ -> c1) CTrue
in gammas, v1
let+ (generalizable, _, v1, ()) =
letn [] (fun _ -> c1) CTrue
in (generalizable, v1)
(* -------------------------------------------------------------------------- *)

View File

@ -31,21 +31,17 @@ open Signatures
elaboration in order to construct an explicitly-typed program. *)
module Make
(X : sig (** @inline *) include TEVAR end)
(S : sig (** @inline *) include GSTRUCTURE end)
(S : sig (** @inline *) include HSTRUCTURE end)
(O : sig (** @inline *) include OUTPUT
with type 'a structure = 'a S.structure end)
: sig
(**A scheme variable [x] is bound by {!def} or by {!let1} and its variants
({!letr1}, {!letn}, {!letrn}) and is referred to by {!instance}. Such a
variable denotes a Hindley-Milner type scheme [σ], or (equivalently) a
constraint abstraction [λα.c], that is, a constraint [c] that is
parameterized with a type variable [α]. *)
(**A scheme variable [x] is bound by {!def}, {!let1}, {!letn}
and is referred to by {!instance}. Such a variable denotes
a Hindley-Milner type scheme σ, or (equivalently) a constraint
abstraction λα.c. *)
type tevar = X.t
type tevars =
tevar list
(* The type ['a structure] of shallow types is provided by [S]
(and repeated by [O]). *)
@ -53,21 +49,12 @@ module Make
are provided by the module [O]. *)
open O
type tyvars =
tyvar list
type tys =
ty list
(**A type variable α denotes an unknown type. The existential quantifier
{!exist} introduces a {i flexible} type variable, whose value can be
chosen so as to satisfy a constraint. The combinators {!(--)} and
{!(---)} allow imposing equality constraints on type variables. *)
type variable
type variables =
variable list
(**A shallow type is a piece of structure whose children are
type variables. *)
type shallow_ty =
@ -79,14 +66,11 @@ module Make
| DeepVar of variable
| DeepStructure of deep_ty structure
(**A decoded scheme consists of a list of quantifiers and a body. The
quantifiers are decoded type variables; the body is a decoded type. The
combinator {!let1} and its variants ({!letr1}, {!letn}, {!letrn}) produce
schemes as part of their semantic value. *)
type scheme = tyvars * ty
type schemes =
scheme list
(**A decoded scheme consists of a list of quantifiers and a body.
The quantifiers are decoded type variables; the body is a decoded type.
The combinators {!let1} and {!letn} produce schemes as part of
their semantic value. *)
type scheme = tyvar list * ty
(* ---------------------------------------------------------------------- *)
@ -176,7 +160,7 @@ module Make
val (let@) : ('a, 'r) binder -> ('a -> 'r co) -> 'r co
(**The binder [exist] creates a fresh type variable and binds it
existentially in the constraint that is being constructed. *)
existentially. *)
val exist: (variable, 'r) binder
(**The binder [shallow τ] is analogous to [exist], but additionally
@ -218,18 +202,19 @@ module Make
(**The constraint [instance x α] requires the type variable [α] to be an
instance of the scheme denoted by the variable [x]. The variable [x]
must have been bound earlier by {!def} or by {!let1} and its variants
({!letr1}, {!letn}, {!letrn}).
must have been bound earlier by {!def}, {!let1}, or {!letn}.
On paper, this constraint is written [x α]. One can also think of
On paper, this constraint is often written [x α]. One can also think of
[x] as a constraint abstraction, in which case this constraint can be
written [x(α)], still on paper.
The semantic value of the constraint [instance x α] is a list of decoded
types. This list indicates how the quantifiers of the scheme denoted by
[x] have been instantiated. The length and order of this list match the
length and order of the quantifiers of the scheme denoted by [x]. *)
val instance: tevar -> variable -> tys co
length and order of the quantifiers of the scheme denoted by [x]. This
scheme is obtained as part of the semantic value of the combinator
{!let1} and {!letn} where [x] is bound. *)
val instance: tevar -> variable -> ty list co
(* ---------------------------------------------------------------------- *)
@ -241,146 +226,62 @@ module Make
equivalent to the equality constraint [α -- β]. *)
val def: tevar -> variable -> 'a co -> 'a co
(**[let1 x c1 c2] binds the term variable [x] to the constraint abstraction
(* [let1 x c1 c2] binds the term variable [x] to the constraint abstraction
[c1] in the constraint [c2]. (Technically, [c1] is a function of a fresh
type variable [α] to a constraint, as in {!exist}.) On paper, we write
[let x = λα.c1(α) in c2] for this constraint.
type variable to a constraint, as in [exist].) The resulting constraint
produces a tuple of 4 results, namely:
- a list [vs] of (decoded) type variables that may appear in [a1], and (hence)
should be universally bound by the client in [a1]. In a typical scenario,
[a1] is a System F term, and the client will build the type abstraction
[\Lambda vs.a1].
- the (decoded) type scheme that was assigned to [x] while solving [c2].
- the value [a1] produced by the constraint [c1].
- the value [a2] produced by the constraint [c2]. *)
val let1: tevar -> (variable -> 'a co) -> 'b co ->
(tyvar list * scheme * 'a * 'b) co
This constraint requires [α.c1(α)] to be satisfied. This is required
even if the term variable [x] is not used in [c2].
(* [let0 c] has the same meaning as [c], but, like [let1], produces a list [vs]
of the type variables that may appear in the result of [c]. *)
val let0: 'a co -> (tyvar list * 'a) co
Inside [c2], an instantiation constraint of the form [x(α')] is logically
equivalent to [c1(α')]. In other words, a [let] constraint acts like a
macro definition: every use of the variable [x] in the scope of this
definition is equivalent to a copy of the constraint abstraction [c1].
(* [letn xs c1 c2] binds [n] term variables [xs] to [n] constraint abstractions
in the constraint [c2]. Here, [c1] is a function of [n] fresh type variables
[vs] to a constraint. The [i]-th term variable, [x_i], ends up bound to the
constraint abstraction of the [i]-th type variable in [c_1], which one could
write [\lambda v_i.c_1]. *)
val letn: tevar list -> (variable list -> 'a co) -> 'b co ->
(tyvar list * scheme list * 'a * 'b) co
The semantic value of this constraint is a tuple of:
- a list [γs] of decoded type variables that may appear in the semantic
value [v1] and therefore should be bound by the user in [v1].
For instance, if the user wishes to build an explicitly-typed
System F term as the result of the elaboration process,
then [v1] will be a System F term,
and the user should construct the abstraction [Λγs.v1],
also a System F term.
The length of the list [γs] cannot be predicted.
The order of its elements is arbitrarily chosen by the solver.
- the decoded scheme assigned to [x] by the solver.
- the semantic value [v1] of the constraint [c1].
- the semantic value [v2] of the constraint [c2]. *)
val let1:
(* x: *) tevar ->
(* c1: *) (variable -> 'a co) ->
(* c2: *) 'b co ->
(tyvars * scheme * 'a * 'b) co
(* [letr1 alphas x (fun alphavs v -> c1) c2] binds the scheme variable [x]
to the constraint abstraction [fun v -> c1] in the contstraint [c2],
where [c1] is also abstracted over a list of rigid variables, one for
each client type variable passed in the list [alphas].
(**[letn] is a more general form of the combinator {!let1}. Like {!let1}, it
is a binary combinator: it has a left-hand side [c1] and a right-hand
side [c2]. However, whereas {!let1} binds one type variable [α] in [c1]
and constructs one scheme, which becomes bound to the variable [x] in
[c2], [letn] binds [n] type variables [αs] in [c1] and constructs [n]
schemes, which become bound to the variables [xs] in [c2].
The resulting constraint produces a tuple of 3 results, namely:
- a list [vs] of (decoded) type variables corresponding to the client type
variables [alphas].
- the value [a1] produced by the constraint [c1].
- the value [a2] produced by the constraint [c2].
The meaning of the constraint [letn xs c1 c2] can be described as follows.
Let [n] stand for the length of the list [xs].
Let [αs] be a list of fresh flexible variables, of the same length.
Let us write [xi] and [αi] for the [i]-th elements of the lists [xs]
and [αs].
Let us write [αs\αi] for the list [αs] deprived of [αi].
Then,
the constraint [letn xs c1 c2] is logically equivalent to
[let xi = λαi.(αs\αi).c1(αs) in c2].
That is, it is equivalent to the constraint [c2],
where each variable [xi] is bound to the
constraint abstraction [λαi.(αs\αi).c1(αs)].
This constraint abstraction has one parameter,
namely, the type variable [αi].
Every other type variable in the list [αs] is considered
existentially bound in this constraint abstraction.
This constraint requires [αs.c1(αs)] to be satisfied. This is required
even if some of the term variables in the list [xs] are not used in [c2].
The semantic value of this constraint is a tuple of:
- a list [γs] of decoded type variables that may appear in the semantic
value [v1] (see {!let1}).
- a list of decoded schemes, in correspondence with the list [xs].
- the semantic value [v1] of the constraint [c1].
- the semantic value [v2] of the constraint [c2].
The combinator [letn] is typically useful when performing type inference
for a construct such as ML's [let p = e1 in e2], where [p] is a pattern.
This construct performs Hindley-Milner generalization and binds several
variables at once, namely the variables defined by the pattern [p]. The
combinator [letn] allows performing generalization and constructing a
scheme for each of the variables defined by [p]. *)
val letn:
(* xs: *) tevars ->
(* c1: *) (variables -> 'a co) ->
(* c2: *) 'b co ->
(tyvars * schemes * 'a * 'b) co
(**The constraint [let0 c] is logically equivalent to [c]. Its semantic
value is a tuple of:
- a list [γs] of decoded type variables that may appear in the semantic
value [v] (see {!let1}).
- the semantic value [v] of the constraint [c].
[let0] can be viewed as a special case of {!letn} where [n] is zero
and where the right-hand constraint [c2] is trivial (that is, true).
The constraint [let0 c] is a {i toplevel constraint}, which means that
it can be passed as an argument to {!solve}. *)
val let0: 'a co -> (tyvars * 'a) co
(**[letr1] is a more general form of the combinator {!let1}. It takes an
integer parameter [k] and binds [k] rigid type variables [βs] in the
left-hand constraint. Like [let1], it also binds a type variable [α]
in the left-hand constraint. Thus, [c1] is a function of [βs] and [α]
to a constraint. On paper, we write [let x = Rβs.λα.c1(βs)(α) in c2].
This constraint requires [βs.α.c1(α)] to be satisfied.
This is required even if the term variable [x] is not used in [c2].
Thus, the variables [βs] are regarded as rigid while [c1] is solved.
Then, while solving [c2], the term variable [x] is bound to
the constraint abstraction [λα.βs.c1(βs)(α)].
In other words, inside [c2], an instantiation constraint of the form
[x(α')] is logically equivalent to [βs.c1(βs)(α')].
At this stage, the variables [βs] are no longer treated as rigid,
and can be instantiated.
The combinator [letr1] helps deal with programming language constructs
where one or more rigid variables are explicitly introduced, such as
[let id (type a) (x : a) : a = x in id 0] in OCaml. In this example,
the type variable [a] must be treated as rigid while type-checking the
left-hand side; then, the term variable [id] must receive the scheme
[a.a a], where [a] is no longer regarded as rigid, so this scheme
can be instantiated to [int int] while type-checking the right-hand
side. *)
val letr1:
(* k: *) int ->
(* x: *) tevar ->
(* c1: *) (variables -> variable -> 'a co) ->
(* c2: *) 'b co ->
(tyvars * scheme * 'a * 'b) co
(**[letrn] subsumes {!let1}, {!letr1}, and {!letrn}.
Like {!letr1}, it takes an integer parameter [k] and binds [k]
rigid type variables [βs] in the left-hand constraint.
Like {!letn}, it takes a list [xs] of term variables and binds a
corresponding list [αs] of type variables in the left-hand constraint.
On paper, we write [let xs = Rβs.λαs.c1(βs)(αs) in c2] for the
constraint that it constructs. *)
val letrn:
(* k: *) int ->
(* xs: *) tevars ->
(* c1: *) (variables -> variables -> 'a co) ->
(* c2: *) 'b co ->
(tyvars * schemes * 'a * 'b) co
Note: unlike [let1], we do not necessarily decode the type scheme
corresponding to [x]; it is less interesting as we know that it
must use exactly the rigid variables [vs] and no other. The
client could still compute the decoded scheme by asking to decode
the witness type of [v] within [c1].
*)
val letr1: 'client_tyvar list
-> tevar
-> (('client_tyvar * variable) list -> variable -> 'a co)
-> 'b co
-> (tyvar list * 'a * 'b) co
val letrn: 'client_tyvar list
-> tevar list
-> (('client_tyvar * variable) list
-> (tevar * variable) list
-> 'a co)
-> 'b co
-> (tyvar list * (tevar * scheme) list * 'a * 'b) co
(* ---------------------------------------------------------------------- *)
(* Correlation with the source code. *)
@ -393,9 +294,8 @@ module Make
(**The constraint [correlate range c] is equivalent to [c], but records that
this constraint is correlated with the range [range] in the source code.
This information is used in error reports. The exceptions {!Unbound},
{!Unify}, {!Cycle}, and {!VariableScopeEscape} carry a range: it is the
nearest range that encloses the abstract syntax tree node where the error
is detected. *)
{!Unify}, and {!Cycle} carry a range: it is the nearest range that
encloses the abstract syntax tree node where the error is detected. *)
val correlate: range -> 'a co -> 'a co
(** {2 Solving Constraints} *)
@ -414,13 +314,6 @@ module Make
is a recursive type: that is, this type involves a μ binder. *)
exception Cycle of range * ty
(**This exception is raised by {!solve} when a rigid variable escapes its
scope, that is, roughly speaking, when one attempts to unify a rigid
variable with a more ancient flexible variable. For example, attempting
to solve the constraints [α. β. α = β] or [α. β. γ. α = β γ]
causes this exception to be raised. *)
exception VariableScopeEscape of range
(**[solve ~rectypes c] determines whether the constraint [c] is satisfiable,
and if so, computes and returns its semantic value. (The constraint [c]
must be closed, so it is satisfiable if and only if it is valid.) If [c]
@ -430,10 +323,9 @@ module Make
can be raised only when [rectypes] is [false].
The constraint [c] must be a {i toplevel constraint}. This means that
every (binding or free) occurrence of a type variable must be wrapped in
{!let0} or in the left-hand side of {!let1} or its variants ({!letr1},
{!letn}, {!letrn}). To turn an arbitrary constraint [c] into a toplevel
constraint, just write [let0 c]. *)
every (binding or free) occurrence of a type variable must appear in the
left-hand side of {!let0}, {!let1}, or {!letn}. To turn an arbitrary
constraint [c] into a toplevel constraint, just write [let0 c]. *)
val solve: rectypes:bool -> 'a co -> 'a
(**/**)

View File

@ -13,8 +13,6 @@ open Signatures
module Option (S : GSTRUCTURE) = struct
module S = S
type 'a structure =
'a S.structure option
@ -54,7 +52,13 @@ module Option (S : GSTRUCTURE) = struct
let s = S.conjunction equate s1 s2 in
if s == s1 then so1 else Some s
let pprint elem os =
PPrint.OCaml.option (S.pprint elem) os
let leaf =
None
let is_leaf =
Option.is_none
let project_nonleaf =
Option.get
end (* Option *)

View File

@ -21,6 +21,11 @@ open Signatures
module Option (S : sig (** @inline *) include GSTRUCTURE end) : sig
(** @inline *)
include GSTRUCTURE_OPT with module S = S
include STRUCTURE_LEAF with type 'a structure = 'a S.structure option
(**[project_nonleaf (Some s)] is [s], while [project_nonleaf None] is
undefined. In other words, if [os] is a non-leaf optional structure,
then [project_nonleaf os] is the underlying structure. *)
val project_nonleaf : 'a structure -> 'a S.structure
end