The type inference problem can be described as, given a context and an expression , find a type such that .
The problem is that, there could be multiple types that is valid in some sense. For example, a function satisfies both the type and intuitively.
In such cases, we want to infer a principal type (I’m using the term “principal” in a loose and informal sense). For example, for the identity function above, we might want to infer something like which could be instantiated to the two concrete types.
Here is another example:
class Animal():
field name :: String
class Cat():
extends Animal
field fishes
class Dog():
extends Animal
field bones
Given the code above, a function fun (x): x.name might have type Cat -> String, Dog -> String, or even Animal -> Object. but a more suitable type would be Animal -> String. So, for different type systems, how we define the property of being “principal” can vary. For a system with parametric polymorphism, it might mean being able to be instantiated to any other possible type; for a system with subtyping, it might mean being the supertype of any other possible type without going too far to the top type like Object unless necessary. In one word, the type we want is principal with regard to a certain relation.
Now let’s consider the type inference for a gradual type system. Still, there could be multiple types that are valid in some sense, and we want to pick a principal one. The problem now is:
- What does “valid” mean?
- What does “principal” mean?
Validity can have many interpretations. It could mean static typability, that is, plugging in a valid type yields a gradually well-typed program. For a unification-based type inference system, that means satisfying all the constraints. It may also concern runtime semantics, such as requiring that after plugging in the inferred type, all executions or at least some executions are safe (no cast error, do not diverge, etc.). For our analysis now, let’s choose the typing-based interpretation, that is, it should at least mean not raising a static type error when plugged in.
What about being principal? Intuitively, just like in systems with subtyping we pick the type satisfying certain properties with regard to the subtyping relation, in a gradual type system we should pick the type with certain properties with regard to the precision or materialization relation. Also like subtyping, the precision or materialization relation induces a upper semilattice on the gradual types. So, the problem becomes: given a set of members of the semilattice where all satisfies the validity condition , pick a satisfying certain properties. Here the relation means is more precise than , or materializes . Note that with that relation and our typability interpretation of validity, has the monotone property: if and , then also .
As a hint, we could try to extract some rules from previous literature (notice that the direction of the order relation in the literature is the reverse of our ):
Rules for gradual type inference [000V]
In section 3 of Gradual Typing with Unification-based Inference, the authors discuss some examples where the naive “well-typed after substitution” approach fails. That implies some rules that gradual type inference should follow.
In the following example codes, α is a type variable not in the parametric polymorphism sense, but in the unification-based type inference sense, that is, a variable to be substituted with a gradual type after type inference.
let f(g: α) = g 1
f 1
The above program would not pass static typecheck, since there is no possible substitution for α. Thus, even if substituting α with ? make the program pass gradual typecheck, such a substitution should not be chosen.
The rule here is that a program can be gradually well-typed if and only if it can be statically well-typed.
Constraint-informativeness preservation
let x: α = x + 1
Substituting α with ? would make the above program pass gradual typecheck, but a more appropriate choice is int.
The rule here is that when a more precise type is possible, a less precise one should not be chosen as the inferred type.
Minimal adequate solution
let f(x: ?) =
let y: α = x in y
Substituting α with some more precise type such as int won’t trigger a type error during gradual typecheck, since they are consistent with ?. However, doing so blocks the possibility to, for example, apply the function to a boolean. The only appropriate substitution for α is ?.
The rule here is that when multiple types all make the program gradually well-typed, then the chosen type should be less precise than them and be consistent with them, that is, they are all materializations of the chosen type.
The first rule is more connected to the Refined Criteria for Gradual Typing: it simply says that if there are no static types in , then we should raise a type error. It implies that has some minimal element(s), i.e. elements that no other elements are smaller than them (different from the least element), and they are all static types since minimal elements that are not static types cannot be in according to rule 1.
The second rule is more like filtering what is “valid”: from the constraints we know that there is a set such that for all and for all , is less precise than . For our specific inference problem to be meaningful, a reasonable requirement is that there exist a lower bound of all with regard to ; otherwise we won’t have a reasonable element to choose as the principal one. That implies that a greatest lower bound of exists, and it is an upper bound of what we might choose as the principal type. From the perspective of types, all the s means some information we already know about the type to infer, and their greatest lower bound is the combination of these informations. For example, we may have , and .
The third rule makes more sense of “principal.” It implies that if the greatest lower bound of does not exist or is not in (i.e. does not have a least element), then the principal element we choose should be greater than or equal to the least upper bound of the minimal elements of . This sets a lower bound of what we might choose as the principal type. Notice that the minimal elements of at least contains some static types (implied by rule 1), and any pair of static types are non-comparable, and any static type is also a minimal element in , so if the greatest lower bound of exists and is in , then that element must be the sole static type in . If that is the case, intuitively this static type should just be the principal type we infer.
The third rule and second rule combined together gives us another requirement: should be less than or equal to . Otherwise we have no reasonable to choose as the principal one. It is also clear that when the two are equal and they are in , they are the principal element to choose.
Are and in ? To answer this, we first ask: in what cases would a type be not in ? Since our notion of “valid” means “not raising type error when plugged in”, then not in , i.e. not valid, should mean it would raise a type error when plugged in, which in turn means that all the materialization of it (thus all static ones) would raise a type error. So, “valid” in turn means some of its materialization (thus some static ones) would fit. This interpretation immediately tells us that and .
Since and , let be the set of all elements in that is between them, form a lattice; more precisely, a sub-lattice of . The next question is: how should we choose the principal type out of it?
If is a singleton, the answer is very simple. In what cases would not be a singleton? That would be the cases where there are materialization of other than that would raise a type error when plugged in. What should we choose as the principal type in that case?
The answer is still not clear to me, but I doubt that it would be more like a design choice. If you want to be more tolerant and allow more things to be consistent, you choose ; if you want to be more precise, you choose .
From the view of abstract interpretation, every gradual type can be concretized to a set of static types , and every set of static types can be abstracted to a gradual type . Obviously, , and .
Also note that this concept of being principal could be somehow orthogonal to other concepts of principal type, such as the subtyping or parametric polymorphism ones we mentioned above. If that is the case, the type inference algorithm need to consider all of them and maybe make some considerations if they are not compatible.