An Extension of HM(X) with Bounded Existential and Universal Data-Types (Full version).pdf

An Extension of HM(X) with Bounded Existential and Universal Data-Types (Full version) Vincent Simonet? Vincent.Simonet@inria.fr Abstract We propose a conservative extension of HM(X), a generic constraint-based type inference framework, with bounded existential (a.k.a. abstract) and universal (a.k.a. polymor- phic) data-types. In the first part of the article, which re- mains abstract of the type and constraint language (i.e. the logic X), we introduce the type system, prove its safety and define a type inference algorithm which computes principal typing judgments. In the second part, we propose a real- istic constraint solving algorithm for the case of structural subtyping, which handles the non-standard construct of the constraint language generated by type inference: a form of bounded universal quantification. 1 Introduction HM(X) is a generic constraint-based type inference system, originally defined for the λ-calculus with let by Odersky, Sulzmann and Wehr [OSW99]. It goes on with the tradi- tion of the Hindley–Milner type system by providing the combination of let-polymorphism and a complete type re- construction algorithm. However, the interest of HM(X) lies in its greater generality: indeed, it is fully parametrized by a logic, X, which is used for expressing types and relating them with constraints. Then, instantiating the framework with different possible logics yields a large variety of type systems. For instance, letting X be the standard Herbrand logic retrieves the usual unification-based Hindley–Milner system. Similarly, choosing a logic equipped with a par- tial order between types yields a type system featuring both subtyping and let-polymorphism. Another contribution of HM(X) resides in its treatment of the typing problem as a constraint. This approach allows modular and systematic definitions of type inference sys- tems, which typically include several orthogonal steps: first, the type system is introduced as a set of logical rules pro- ducing typ