Commit 97a40e87 authored by Gabriel Scherer's avatar Gabriel Scherer
Browse files

Robust schemes by generalization without a generic rank

A delicate aspect of Inferno's implementation of generalization is
that its notion of "scheme" is not robust, in the sense that:

- Computing the set of structureless variables of a polymorphic scheme
  may give an incorrect result if performed too late (after other levels
  have been generalized), it must be performed right after
  generalization.

- Similarly, the implementation of instantiation is fragile: if
  a scheme comes from level N+1, instantiation constraints at level
  N work as expected, but trying to instantiate the scheme at level N-1
  or below may give incorrect results.

Neither of those aspects are problematic for inference in a core ML
language: consider `let x = t in u`, all instantiation constraints
for `x` (whose scheme is the type of `t` at some level N+1) come from
syntactic occurrences of `x` in `u`, at level N.

However it could be problematic when considering other language
features:

- Frozen constraints may result in partially-frozen polymorphic
  schemes (some parts of a polymorphic schemes are not generic, as their
  type still needs to be determined by unfreezing some
  frozen constraints) for which computing the set of quantifiers right
  away is impossible. We need to be able to revisit the scheme later,
  after all parts are unfrozen, to compute the quantified variables.

- First-class polymorphism lets you export a polymorphic scheme
  outside the syntactic scope of the let-body, so that a scheme from
  level N+2 may be instantiated at level N or below. Consider for
  example:

       let foo (y : 'b) = (* level N+1 *)
          {m : 'a . 'a -> 'a * 'b =
            (* level N+2 *)
            fun x -> (x, y)
          }
       in (* level N *) (foo t).m u

To solve this problem, I propose to keep the rank of generic
variables. Currently generalization is performed by modifying
generalized variables to give them an "infinite" level
`Generalization.generic`. Instead, we use a separate boolean flag
`mutable generic: bool` that starts `false` and is set to `true`
during generalization.

A scheme is a pair of a root variable, and the rank at which the
scheme was generalized. To instantiate a type scheme, we simply copy
the transitive children of the root variables that are generic, and
share the non-generic variables.

Generic variables keep the level they come from, and in particular we
define the quantified variables of a scheme as the set of generic
structureless variables *at the level of the scheme*, rather than some
lower level. In the example above, the generic type `'a -> 'a * 'b)`
has `'a` at level N+2 and `'b` at level N+1, so type scheme of
`m` (coming from level N+2) can be correctly computed as just
`'a. 'a -> 'a * 'b`.

(To embed a variable/type at level N as a trivial "monomorphic scheme"
with no polymorphism, we simply build a scheme of level N+1 on this variable.)

Remark on level (non)confusion
------------------------------

There is a subtlety due to the use of a linear array of generalization
regions, rather than a tree of regions: two generalization regions may
have the same integer 'rank' yet be distinct. In particular, it would
be very wrong (unsound) to start unifying flexible (non-generic)
variables living in different generalization regions at the same
level; let us call this a "level confusion" problem.

With our proposed approach to generalization, it is possible to have
both *generic* variables at some level L and non-generic variables at
level Lor above, and to instantiate generic variables from L at some
equal or higher level. Consider for example:

    (* level N *)
    let id = (* level N+1 *) fun x -> x in
    let f x =
      (* another region at level N+1 *)
      let g y =
        ... id (x, y) ...
      in ...
    in ...

The instantiation constraint on `id x` then involves copying generic
nodes of level N+1 into flexible nodes at level N+2. This sounds a bit
fishy at first; it sounds like we could have a level confusion problem.

This example is in fact perfectly fine: irrelevant after
instantiation, as the copies are made at the level of the instance, so
the generic variables of level N are copied into flexible variables at
level N+2 (not flexible variables of level N or anything like that);
besides, both the scheme and the instantiation site may contain
flexible variables of level N or below, but in this case they come
from the exact same generalization regions, there is no level
confusion.

In general, we instantiate a scheme coming from generalization region
RA at level A into a generalization region RB at level B (which may be
higher or lower than A. Consider the region RC at level C (C < A,
C <= B) that is the nearest common ancestor of RA and RB in the tree
of generalization regions.

If RB is an active descendant of RC, all siblings of RC that are not
ancestors of RC must have been generalized. In particular, all regions
on the path between RC and RA have been generalized, and their
variables in the scheme are now generic. Thus a flexible variable
reachable from the scheme must have level <= C. The ancestors of RA
and RB at level <= C are below their nearest common ancestor RC, so
they are exactly the same region: there is no level confusion for
flexible variables.
parent aa48cc37
Pipeline #259344 passed with stage
in 8 minutes and 18 seconds
......@@ -25,17 +25,16 @@ module S = struct
TyConstr (tid, ts)
(* Note: we enforce the same traversal order for 'fold'
as for 'map' and 'iter' *)
let fold f t accu =
match t with
| TyArrow (t1, t2) ->
let accu = f t1 accu in
let accu = f t2 accu in
accu
| TyProduct ts ->
List.fold_right f ts accu
| TyConstr (_, ts) ->
List.fold_right f ts accu
| TyProduct ts | TyConstr (_, ts) ->
List.fold_left (fun accu t -> f t accu) accu ts
let iter f t =
let _ = map f t in
......
......@@ -41,6 +41,7 @@ let test_with_log ~log (env : ML.datatype_env) (t : ML.term) : bool =
assert (t = t');
let outcome_env =
ML2F.translate_env env in
Printf.ksprintf (Log.log_msg log) "Input term:\n%s\n" s;
let outcome =
Log.attempt log
"Type inference and translation to System F...\n"
......
......@@ -391,3 +391,17 @@ let test_match_some_annotated =
| (Some _ : some 'a. option 'a) -> None
end"
match_some_annotated
(** Regressions *)
let ast_from_string s =
let lexbuf = Lexing.from_string s in
MLParser.self_contained_term MLLexer.read lexbuf
let regression1 =
let t = ast_from_string "let x1 = (...[], ...[]) in ...[] x1" in
test Datatype.Env.empty t
let regression2 =
let t = ast_from_string "let f = fun x -> let g = fun y -> (x, y) in g in fun x -> fun y -> f" in
test Datatype.Env.empty t
......@@ -25,37 +25,49 @@ module Make (S : STRUCTURE) = struct
type rank = int
module Rank = struct
type t = rank
let merge d1 d2 : t = min d1 d2
let merge r1 r2 : t = min r1 r2
let equal (r1 : t) (r2 : t) = Int.equal r1 r2
let base = 0
let dummy = (-1)
let is_dummy r = equal r dummy
let () =
(* we index into an array starting from the base rank,
so we better have (base >= 0). *)
assert (base >= 0)
end
(* The constant [generic] is defined as [-1]. This rank is used for the variables
that form the generic (to-be-copied) part of a type scheme. *)
let generic =
-1
(* The rank [no_rank] is defined as [0]. This rank is used when a variable is
freshly created and is not known to us yet. *)
let no_rank =
0
(* The positive ranks are valid indices into the pool array. *)
let base_rank =
no_rank + 1
module Data = struct
type t = {
mutable rank: int;
mutable generic: bool;
}
let dummy () = { rank = Rank.dummy; generic = false }
let merge d1 d2 =
assert (not (Rank.is_dummy d1.rank));
assert (not (Rank.is_dummy d2.rank));
assert (not d1.generic);
assert (not d2.generic);
let rank = Rank.merge d1.rank d2.rank in
{ rank; generic = false; }
end
module U = Unifier.Make(S)(Rank)
module U = Unifier.Make(S)(Data)
let fresh s = U.fresh s no_rank
let fresh s =
U.fresh s (Data.dummy ())
let rank (v : U.variable) : rank = U.data v
let set_rank (v : U.variable) (r : rank) = U.set_data v r
let rank (v : U.variable) : rank = (U.data v).Data.rank
let set_rank (v : U.variable) (r : rank) = (U.data v).Data.rank <- r
let adjust_rank (v : U.variable) (r : rank) =
(* equivalent to [set_rank v (min r (rank v))] *)
if r < rank v then set_rank v r
let is_generic (v : U.variable) : bool = (U.data v).Data.generic
let set_generic (v : U.variable) = (U.data v).Data.generic <- true
(* The rank of a variable is set to the current rank when the variable is
first created. During the lifetime of a variable, its rank can only
decrease. Decreasing a variable's rank amounts to hoisting out the
......@@ -104,71 +116,77 @@ type state = {
rank [state.young] is decremented by one, and all variables whose rank was
precisely [state.young] become universally quantified, or generic. These
variables are no longer stored in any pool, as they are no longer
existentially quantified. Their rank is set to the constant [generic].
This allows [instantiate] to recognize them easily. *)
existentially quantified. *)
(* The generic variables that have no structure are the ``quantifiers'' of the
type scheme. A type scheme is internally represented as a pair of a list of
quantifiers and a root variable, the ``body''. The order of the quantifiers
is arbitrarily chosen, but once fixed, matters; the functions [quantifiers]
and [instantiation] must agree on this order. The quantifiers are exactly
the variables that are reachable from the body, have rank [generic], and
have no structure. *)
(* Technical note (mostly to myself). The representation of type schemes is
not stable, in the following sense. When a scheme is first created, its
universal quantifiers versus free variables are recognized by their rank
(rank [generic], versus a positive rank). This remains valid as long as
this type scheme is in scope, i.e., as long as the current rank does not
decrease below its current value. However, the current rank ultimately
decreases (all the way down to zero), and at this final point, all
variables have rank [generic], so the type schemes that were previously
created are no longer useable. We could fix this problem (if desired) by
not relying on the rank within [instantiate]; we would instead rely on a
list of all generic variables (with or without structure). Note: the
field [quantifiers] is a list of the generic variables *without* structure. *)
(* TEMPORARY consider doing this? maybe benchmark.
If we DON'T do it, then we should document the fact that [instantiate]
won't work any more after the current rank decreases below its current
value. (Not really a problem, as the end-end-user is not supposed to
have access to this function.) *)
type scheme = {
(* A list of quantifiers. *)
quantifiers: U.variable list;
(* A distinguished variable forms the body of the type scheme. *)
body: U.variable
}
type scheme. A type scheme is internally represented as a pair of a root variable,
and the rank at which generalization took place. In particular, the quantifiers
can be reconstructed by traversing the root to find all structureless variable
at the current level. Generic variables of a lower level are not part of the
current scheme, they were generalized later during inference. *)
type scheme = { root: U.variable; rank : Rank.t; }
(* -------------------------------------------------------------------------- *)
(* The initial state. *)
(* The pool array is initially populated with empty pools. The current rank is
initially set to 0, so the first rank that is actually exploited is 1. *)
(* The pool array is initially populated with empty pools. The rank is
chosen so that the rank of its first child, the first rank that is
actually exploited, is Rank.base. *)
let init () = {
pool = InfiniteArray.make 8 [];
young = no_rank;
young = Rank.base - 1;
}
(* -------------------------------------------------------------------------- *)
(* Accessors for type schemes. *)
(* To get a "trivial" (fully monomorphic) type scheme,
we pick a rank strictly above the root variable rank. *)
let trivial body =
{ root = body; rank = rank body + 1 }
let quantifiers { quantifiers; _ } =
quantifiers
let body { root; _ } = root
let body { body; _ } =
body
(* The quantifiers of a type scheme are exactly the generic
structureless variables that are reachable from the root, at the
scheme rank. *)
let quantifiers { root; rank = scheme_rank } =
(* -------------------------------------------------------------------------- *)
(* Prepare to mark which variables have been visited. *)
let visited : unit U.VarMap.t = U.VarMap.create 128 in
(* A trivial constructor of type schemes. *)
let rec traverse v quantifiers =
let trivial body =
{ quantifiers = []; body }
(* If this variable is not generic or has been discovered already, then
we must stop. *)
if not (is_generic v)
|| not (Rank.equal (rank v) scheme_rank)
|| U.VarMap.mem visited v
then
quantifiers
else begin
(* Mark this variable as visited. If it carries no structure, then it is
a leaf in the generic part of this type scheme, that is, a
quantifier: add it to the list of quantifiers. Otherwise, traverse
its descendants. Note that the variable must be marked before the
recursive call, so as to guarantee termination in the presence of
cyclic terms. *)
U.VarMap.add visited v ();
(* The order in which the quantifiers appear is determined in an arbitrary
manner. *)
match U.structure v with
| None ->
v :: quantifiers
| Some t ->
S.fold traverse t quantifiers
end
in
traverse root []
(* -------------------------------------------------------------------------- *)
......@@ -178,20 +196,20 @@ let trivial body =
let register_at_rank ({ pool; _ } as state) v =
let r = rank v in
assert (0 < r && r <= state.young);
assert (Rank.base <= r && r <= state.young);
InfiniteArray.set pool r (v :: InfiniteArray.get pool r)
(* The external function [register] assumes that [v]'s rank is uninitialized.
It sets this rank to the current rank, [state.young], then registers [v]. *)
let registered v =
not (Rank.is_dummy (rank v))
let register state v =
assert (rank v = no_rank);
assert (not (registered v));
set_rank v state.young;
register_at_rank state v
let registered v =
rank v <> no_rank
(* -------------------------------------------------------------------------- *)
(* Debugging utilities. *)
......@@ -207,7 +225,7 @@ let show_young state =
Printf.printf "state.young = %d\n" state.young
let show_pools state =
for k = base_rank to state.young do
for k = Rank.base to state.young do
show_pool state k
done
......@@ -227,53 +245,6 @@ let enter state =
(* -------------------------------------------------------------------------- *)
(* The internal function [make_scheme] turns a variable, [body], into a type
scheme. The body of the type scheme is [body]. The quantifiers of the type
scheme are exactly the generic structureless variables that are reachable,
in the unification graph, from [body]. The function [is_generic] determines
which variables are generic. *)
(* The order in which the quantifiers appear is determined in an arbitrary
manner. *)
let make_scheme (is_generic : U.variable -> bool) (body : U.variable) : scheme =
(* Prepare to mark which variables have been visited. *)
let visited : unit U.VarMap.t = U.VarMap.create 128 in
let rec traverse v quantifiers =
(* If this variable is not generic or has been discovered already, then
we must stop. *)
if not (is_generic v) || U.VarMap.mem visited v then
quantifiers
else begin
(* Mark this variable as visited. If it carries no structure, then it is
a leaf in the generic part of this type scheme, that is, a
quantifier: add it to the list of quantifiers. Otherwise, traverse
its descendants. Note that the variable must be marked before the
recursive call, so as to guarantee termination in the presence of
cyclic terms. *)
U.VarMap.add visited v ();
match U.structure v with
| None ->
v :: quantifiers
| Some t ->
S.fold traverse t quantifiers
end
in
(* Discover which quantifiers are accessible from [body]. *)
let quantifiers = traverse body [] in
(* Build a type scheme. *)
{ quantifiers; body }
(* -------------------------------------------------------------------------- *)
(* [exit] is where the moderately subtle generalization work takes place. *)
(* A data structure to represent all the variables created at the youngest level.
......@@ -318,7 +289,7 @@ let young_variable_generation state =
List.iter (fun v ->
U.VarMap.add table v ();
let r = rank v in
assert (0 < r && r <= state.young);
assert (Rank.base <= r && r <= state.young);
by_rank.(r) <- v :: by_rank.(r)
) vs;
......@@ -355,12 +326,12 @@ let update_generation_ranks young_generation =
let visited : unit U.VarMap.t = U.VarMap.create 128 in
for k = base_rank to young_generation.level do
for k = Rank.base to young_generation.level do
(* A postcondition of [traverse v] is [U.rank v <= k]. (This is downward
propagation.) *)
let rec traverse v =
assert (rank v > 0);
assert (rank v >= Rank.base);
(* If [v] was visited before, then its rank must be below [k], as we
adjust ranks on the way down already. *)
if U.VarMap.mem visited v then
......@@ -389,7 +360,7 @@ let update_generation_ranks young_generation =
S.fold (fun child accu ->
traverse child;
max (rank child) accu
) t base_rank (* the base rank is neutral for [max] *)
) t Rank.base (* the base rank is neutral for [max] *)
)
) (U.structure v)
end
......@@ -403,9 +374,6 @@ let update_generation_ranks young_generation =
done
let is_generic v =
rank v = generic
let generalize state young_generation : U.variable list =
(* Every variable that has become an alias for some other (old or young)
variable is dropped. We keep only one representative of each class.
......@@ -427,7 +395,7 @@ let generalize state young_generation : U.variable list =
end
else begin
assert (rank v = state.young);
set_rank v generic;
set_generic v;
U.structure v = None
end
end
......@@ -476,40 +444,40 @@ let exit ~rectypes state roots =
(* Exit the current inference level. *)
state.young <- state.young - 1;
let make_scheme root = { root; rank = young_generation.level; } in
(* Return the list of unique generalizable variables that was constructed
above, and a list of type schemes, obtained from the list [roots]. *)
generalizable,
List.map (make_scheme is_generic) roots
List.map make_scheme roots
(* -------------------------------------------------------------------------- *)
(* Instantiation amounts to copying a fragment of a graph. The fragment that
must be copied is determined by inspecting the rank -- [generic] means
copy, a positive rank means don't copy. *)
must be copied is exactly the prefix which satisfies [is_generic]. *)
let instantiate state { quantifiers; body } =
let instantiate state { root; rank = scheme_rank } =
(* Prepare to mark which variables have been visited and record their copy. *)
let visited : U.variable U.VarMap.t = U.VarMap.create 128 in
let quantifier_instances = ref [] in
(* If the variable [v] has rank [generic], then [copy v] returns a copy of
it, and copies its descendants recursively. If [v] has positive rank,
then [copy v] returns [v]. Only one copy per variable is created, even if
a variable is encountered several times during the traversal. *)
let rec copy v =
(* If this variable has positive rank, then it is not generic: we must
stop. *)
if rank v > 0 then
if not (is_generic v) then
v
(* If a copy of this variable has been created already, return it. *)
else begin
assert (rank v = generic);
try
U.VarMap.find visited v
with Not_found ->
......@@ -520,15 +488,55 @@ let instantiate state { quantifiers; body } =
recursive call to [copy], so as to guarantee termination in the
presence of cyclic terms. *)
let v' = U.fresh None state.young in
let v' =
let data = { Data.rank = state.young; Data.generic = false } in
U.fresh None data in
register_at_rank state v';
U.VarMap.add visited v v';
U.set_structure v' (Option.map (S.map copy) (U.structure v));
begin match U.structure v with
| None ->
(* When inferring Core ML terms, the condition on ranks below is
not necessary: a term (let x = t in u) will only ever generate
instance constraints for (x) in the constraint elaborated for (u).
These instance constraints always take place at the level right below
the level of (t), before this level has been generalized. At this point,
no lowever-level variables could ever be generic.
The condition is necessary to support other language features,
such as various forms of first-class polymorphism:
let p = fun y ->
{ id : 'a. 'a -> 'a * 'b = fun x -> (x, y) }
in
p.id ()
In this example, the use of
p.id
at level 0 ccreates an instance constraint on a polymorphic scheme
('a . 'a -> 'a * 'b) coming from level 2 { id = ... }, and at this point
the level 1 (let p = ...) also contains generic variables: if we
collected all generic structureless variables, we would instead
produce the scheme ('a 'b. 'a -> 'a * 'b), which is incorrect.
*)
if Rank.equal (rank v) scheme_rank then
quantifier_instances := v' :: !quantifier_instances;
| Some s ->
U.set_structure v' (Some (S.map copy s));
end;
v'
end
in
List.map copy quantifiers, copy body
(* [Gabriel]: we are assuming here that quantifiers will be computed in the same order in this function
and in 'quantifiers' above. This is fairly optimistic, as it relies on two facts:
- the iteration order of the provided S.map and S.fold are the same
- the 'copy' traversal traverses more than 'quantifiers', as it also descendes in
generic nodes at lower level, but this does not affect the traversal order of
current-level nodes as older nodes can never reach current-level nodes
Caching the list of quantifiers may be a more robust design, but here we really wanted to verify
our idea that the generic-with-levels design allows for after-the-fact computation of quantifiers.
*)
let instance = copy root in
!quantifier_instances, instance
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment