Gradual Typing Reading Notes [000T]

  • April 01, 2026

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.

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.

        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:

          1. 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.
          2. 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”.

          Related

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

          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.