An extension of HM(X) with bounded existential and universal data-types

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. polymorphic) data-types. In the first part of the article, which restract 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 realistic 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.

• Type: Conference
• Year: 2003
• Where: ICFP
• Authors: Vincent Simonet
• Keywords: Constraint Solving Algorithm, Constraint-based Type Inference, ICFP 2003, Programming Languages, Type Inference Algorithm