Rules for gradual type inference [000V]

April 21, 2026

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.

Static conservativity

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.

Contexts

Gradual Typing Reading Notes [000T]

April 01, 2026

Rules for gradual type inference [000V]

Static conservativity

let f(g: α) = g 1
f 1

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

Notes on Gradual Type Inference

ArticleDynamic Type Inference for Gradual Hindley–Milner Typing [msi-Dynamictypeinference-2019]

Proc. ACM Program. Lang. 3
Yusuke Miyazaki, Taro Sekiyama, Atsushi Igarashi
2019-01-02
10.1145/3290331

Garcia and Cimini study a type inference problem for the ITGL, an implicitly and gradually typed language with let-polymorphism, and develop a sound and complete inference algorithm for it. Soundness and completeness mean that, if the algorithm succeeds, the input term can be translated to a well-typed term of an explicitly typed blame calculus by cast insertion and vice versa. However, in general, there are many possible translations depending on how type variables that were left undecided by static type inference are instantiated with concrete static types. Worse, the translated terms may behave differently—some evaluate to values but others raise blame. In this paper, we propose and formalize a new blame calculus λBDTI that avoids such divergence as an intermediate language for the ITGL. A main idea is to allow a term to contain type variables (that have not been instantiated during static type inference) and defer instantiation of these type variables to run time. We introduce dynamic type inference (DTI) into the semantics of λBDTI so that type variables are instantiated along reduction. The DTI-based semantics not only avoids the divergence described above but also is sound and complete with respect to the semantics of fully instantiated terms in the following sense: if the evaluation of a term succeeds (i.e., terminates with a value) in the DTI-based semantics, then there is a fully instantiated version of the term that also succeeds in the explicitly typed blame calculus and vice versa. Finally, we prove the gradual guarantee, which is an important correctness criterion of a gradually typed language, for the ITGL.

My feeling is that the problems described in section 1.3 and section 1.4 of this paper are somehow not as severe as they might initially appear. The problem is basically that some programs left you so-called undecided type variables, which can be instantiated to any type; these undecided type variables are usually introduced due to the presence of the $?$ type, which hides useful information from other parts of the program. This brings two problems:

If you fill in the undecided type variables with some concrete types, the program will reduce to a value, while some other choices of types will lead to divergence.
Even if you fill in the undecided type variables with the $?$ type, that would allow the program even if there are no static types that make the program execution successful.

Actually, both of the problems seems to be the inherent problems of gradual typing — if you hide too much information using $?$ types, the inference will not be able to give useful results. (Maybe that is why the authors choose a “dynamic inference” approach.) For the first problem, I don’t think there are good solutions (maybe see papers by Castagna et al. recently for how they intersect the dynamic type with the static types to get more precise inference results) other than the approach of the second problem. For the second problem, I think the core of the erroneous example by the authors is that the static type system of their language is not strong enough: add union types and the problem will be solved for their example. Plus, I think the point of using dynamic types is, sometimes, to allow some programs that are not statically well-typed but are still “safe”.

Weeknotes 17, Apr 2026 [2026-W17]

April 21, 2026

This week I have been thinking about the problem of choosing a “best” or “principal” type when performing gradual type inference.

Principal type for gradual type inference

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 $𝖨𝗇𝗍 \to 𝖨𝗇𝗍$ and $𝖡𝗈𝗈𝗅 \to 𝖡𝗈𝗈𝗅$ 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 $\forall 𝛼 . 𝛼 \to 𝛼$ 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 $⟨ 𝑆, \leq ⟩$ where all $𝑡 \in 𝑇$ satisfies the validity condition $𝑉 (𝑡)$ , pick a $𝑡 \in 𝑇$ satisfying certain properties. Here the relation $𝑎 \leq 𝑏$ means $𝑎$ is more precise than $𝑏$ , or $𝑎$ materializes $𝑏$ . Note that with that relation and our typability interpretation of validity, $𝑉 (𝑡)$ has the monotone property: if $𝑉 (𝑡_{1})$ and $𝑡_{1} \leq 𝑡_{2}$ , then also $𝑉 (𝑡_{2})$ .

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 $\leq$ ):

Rules for gradual type inference [000V]

Static conservativity

let f(g: α) = g 1
f 1

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

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 $Σ \subseteq 𝑆$ such that for all $𝑡 \in 𝑇$ and for all $𝜎 \in Σ$ , $𝜎$ is less precise than $𝑡$ . For our specific inference problem to be meaningful, a reasonable requirement is that there exist a lower bound of all $𝜎 \in Σ$ with regard to $\leq$ ; 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 $Σ = {? \to (𝖨𝗇𝗍 \to ?), ? \to (? \to 𝖨𝗇𝗍)}$ , and $𝜎_{𝗀𝗅𝖻} = ? \to (𝖨𝗇𝗍 \to 𝖨𝗇𝗍)$ .

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 $\overset{̆}{𝑡}$ of the minimal elements of $𝑇$ . This $\overset{̆}{𝑡}$ 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 $⟨ 𝑆, \leq ⟩$ , 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: $\overset{̆}{𝑡}$ 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 $\overset{̆}{𝑡}$ 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 $𝜎_{𝗀𝗅𝖻} \in 𝑇$ and $\overset{̆}{𝑡} \in 𝑇$ .

Since $𝜎_{𝗀𝗅𝖻} \in 𝑇$ and $\overset{̆}{𝑡} \in 𝑇$ , let $𝑇^{'} \subseteq 𝑇$ be the set of all elements in $𝑇$ that is between them, $⟨ 𝑇, \leq ⟩$ form a lattice; more precisely, a sub-lattice of $⟨ 𝑆, \leq ⟩$ . 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 $\overset{̆}{𝑡}$ 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 $\overset{̆}{𝑡}$ .

From the view of abstract interpretation, every gradual type $𝜏$ can be concretized to a set of static types $𝛾 (𝜏)$ , and every set of static types ${𝑡, \dots}$ can be abstracted to a gradual type $𝛼 ({𝑡, \dots})$ . Obviously, $𝜎_{𝗀𝗅𝖻} = 𝛼 (⋃_{𝑡 \in 𝑇} 𝛾 (𝑡))$ , and $\overset{̆}{𝑡} = 𝛼 (⋂_{𝑡 \in 𝑇} 𝛾 (𝑡))$ .

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.

InproceedingsGradual Typing with Unification-based Inference [sv-GradualTypingUnificationbased-2008]

DLS '08
Jeremy G. Siek, Manish Vachharajani
2008-07-08
10.1145/1408681.1408688

Static and dynamic type systems have well-known strengths and weaknesses. Gradual typing provides the benefits of both in a single language by giving the programmer control over which portions of the program are statically checked based on the presence or absence of type annotations. This paper studies the combination of gradual typing and unification-based type inference with the goal of developing a system that helps programmers increase the amount of static checking in their program. The key question in combining gradual typing and type inference is how should the dynamic type of a gradual system interact with the type variables of a type inference system. This paper explores the design space and shows why three straightforward approaches fail to meet our design goals. This paper presents a new type system based on the idea that a solution for a type variable should be as informative as any type that constrains the variable. The paper also develops an efficient inference algorithm and proves it sound and complete with respect to the type system.