A Type Inference System Based on Saturation of Subtyping Constraints

Abstract

This paper (This work is part of the first author’s Ph.D. thesis [15].) presents a powerful and flexible technique for defining type inference algorithms, on an ML-like language, that involve subtyping and whose soundness can be proved. We define a typing algorithm as a set of inference rules of three distinct forms: typing rules collect subtyping constraints to be satisfied, instantiation rules instantiate type schemes, and saturation rules specify how to check the validity and consistency of collected constraints. Essentially, type inference then proceeds in two intertwined phases: one that extracts constraints and the other that saturates the sets of constraints. Our technique extends easily to the treatment of high-level features such as polymorphism, overloading, variants and pattern-matching, or generalized algebraic data types (GADTs).

A Appendix

We give here the complete set of rules for the language given in Fig. 1.

Meta-functions

The T meta-function associates a type scheme to constants and primitives. For instance:

• 
• 

Typing

Instantiation

Saturation

To prevent our algorithm from entering an infinite loop in the presence of cyclic relations between type variables, before checking the compatibility of a constraint with $\varPhi$, we check whether this constraint is already present in $\varPhi$. If not, one of SNewConstraint($\leqslant$) or SNewConstraint($\nleqslant$) is used, and we add the new constraint in $\varPhi$ and generate a property annotated with a question mark ($\vdash ^{\!\!\!\!\tiny ?\,}$) consumed by rules defined further. If so, one of the axioms SAlreadyProved($\leqslant$) or SAlreadyProved($\nleqslant$) is used and no more constraint is generated.