(Gentle ping: this is not a pressing issue, as no development that I would be trying to upstream depends on this change, but I still wonder what you think with my more detailed response.)
SCHERER Gabriel (a1d83bd9) at 22 Jun 08:13
SCHERER Gabriel (8d89520d) at 22 Jun 08:13
Merge branch 'F-annot' into 'master'
... and 3 more commits
Before this MR, the ML program (t : some a . ty)
would elaborate into elab((t : some a. ty)) := elab(t)
.
This can hide issues with the inference engine; for example our inference engine could have just completely ignored annotations, and you would never notice the difference on well-typed programs. (We mostly test using well-typed programs, especially in the random generator.)
@omartino and myself are starting to work on rigid variables, and there the question of elaborating annotations becomes even more interesting: we want an elaboration for (fun x -> x : for a. a -> a)
that enforces polymorphism in the elaborated System F term -- (Fun a. fun (x:a) -> x : forall a. a -> a) [tau]
for tau
the instantiation witness.
In preparation for these questions, the current MR introduces annotations in System F, and elaborates ML annotations into System F annotations. We now have elab(t : some a. ty) := (elab(t): elab(ty)[tau/a])
, where tau
is the witness of a
. (One could add type-level lets and elaborate into (elab(t) : let a = tau in elab(ty))
to respect sharing, but I did not bother.)
I don't really understand what problem you are trying to solve, or what future problem you are planning to avoid.
I would like to be able to reconstruct the set of quantifiers of a scheme, at any later point during or after constraint resolution.
Ranks so far have a logical meaning: they indicate where the variable is bound (by an existential quantifier).
With the new approach, a variable is either "flexible" or "generic". Only flexible variables are logically bound to existential quantifiers, and their rank indicates the nesting depth of (let x = [] in u) frames in the constraint around them -- they are existentially bound at the nearest such frame. For generic variables, the rank also relates to where they are bound, it indicates the depth in the constraint at which their (let x : sigma in []) frame is located -- they are universally bound in the "sigma" there, whose rank is defined to be 1 + the let-nesting-rank of the frame itself.
The variables in scope of the scheme "sigma" are its own universal variables, and the existential variables that are bound below it in the constraint. In particular, any existential variable has a strictly lower rank than the scheme itself, so only its universal variables have the scheme rank.
In particular, the construction of a monomorphic scheme corresponds to the solving step (in the notation of your "the essence of ML type inference" paper)
S; U; (def x : X in C) ~> S[let x : X in []]; U; C
which suggests taking the rank of "X as a scheme" to be 1 + the current rank. The current implementation instead uses 1 + rank(X), which corresponds to placing the (let x : tau in []) frame not at the top of the constraint, but directly inside the frame in which X itself is bound.
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
(at 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.)
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: the level of generic variables irrelevant after instantiation, as the copies are made at the level of the instance. In this example 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 descendants of RC that are not ancestors of RB 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.
SCHERER Gabriel (97a40e87) at 12 Jun 16:26
Robust schemes by generalization without a generic rank
... and 168 more commits
SCHERER Gabriel (aa48cc37) at 12 Jun 05:41
minor fixes
This work-in-progress MR adds better support for syntax errors in the parser -- the basic feature of printing the faulty location. However it appears that I got something wrong, as the column locations printed seem incorrect. I ran out of time to fix the issues (more exciting Inferno things to hack on!), so I'm sending the MR as a draft in the hope that I will be motivated to investigate and improve it later.
I'm seeing a lot of parsing errors these last few weeks, because @omartino implemented a check that the pretty-printer and parsers roundtrip (in TestMLRandom). In practice quite often I get one of them wrong (it happened to me for typed holes for example) and the random generator finds the bug. But debugging syntax errors occurring in the pretty-printing of randomly-generated program is difficult, as I don't know the source in the first place. This MR is supposed to improve the situation slightly, but in practice things are still fairly painful, and I am not sure how to improve. (I think that showing the full line of input that is faulty, with the error part underlined, would be helpful to locate where in the grammar the issue is, but this is way over my current error-message complexity budget.)
Before this MR, the ML program (t : some a . ty)
would elaborate into elab((t : some a. ty)) := elab(t)
.
This can hide issues with the inference engine; for example our inference engine could have just completely ignored annotations, and you would never notice the difference on well-typed programs. (We mostly test using well-typed programs, especially in the random generator.)
@omartino and myself are starting to work on rigid variables, and there the question of elaborating annotations becomes even more interesting: we want an elaboration for (fun x -> x : for a. a -> a)
that enforces polymorphism in the elaborated System F term -- (Fun a. fun (x:a) -> x : forall a. a -> a) [tau]
for tau
the instantiation witness.
In preparation for these questions, the current MR introduces annotations in System F, and elaborates ML annotations into System F annotations. We now have elab(t : some a. ty) := (elab(t): elab(ty)[tau/a])
, where tau
is the witness of a
. (One could add type-level lets and elaborate into (elab(t) : let a = tau in elab(ty))
to respect sharing, but I did not bother.)
SCHERER Gabriel (a1d83bd9) at 11 Jun 19:28
TestMLRandom: generate trivial annotations
... and 169 more commits
SCHERER Gabriel (7575df98) at 11 Jun 19:25
WIP: print syntax error locations
... and 167 more commits
SCHERER Gabriel (eedfd95c) at 10 Jun 16:19
SCHERER Gabriel (e6953c62) at 10 Jun 16:19
Merge branch 'typed-holes' into 'master'
... and 6 more commits
A typed hole can have any type (it imposes no typing constraints on the context around it), and its subterms can have any type (the hole imposes no constraint on them).
This is the ultimate language construct to do type-preserving shrinking. When shrinking it is important to be able to remove subterms that do not participate to the error.
Holes with no subterms can be used to completely erase a term. Holes with subterms can be used to selectively erase parts of a term (for example, the application "t u" can be rewritten into the hole "...[t, u]", erasing only the application rule).
The MR also contains some independent improvements to the shrinking strategy; in particular convenient shrinking for products, which I hope to possibly upstream in QCheck directly.
It depends what we assume of Inferno users: do they access SolverLo? But the PR does not touch SolverHi.mli, so someone that would only use the high-level interface should see no change.