An extension of HM(X) with bounded existential and universal data-types
- 25 August 2003
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 38 (9) , 39-50
- https://doi.org/10.1145/944746.944710
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. polymorphic) data-types. In the first part of the article, which remains 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 realistic constraint solving algorithm for the case of structural sub-typing, which handles the non-standard construct of the constraint language generated by type inference: a form of bounded universal quantification.This publication has 13 references indexed in Scilit:
- An extension of HM(X) with bounded existential and universal data-typesPublished by Association for Computing Machinery (ACM) ,2003
- ML FPublished by Association for Computing Machinery (ACM) ,2003
- Subtype inequalitiesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Information flow inference for MLACM Transactions on Programming Languages and Systems, 2003
- Colored local type inferenceACM SIGPLAN Notices, 2001
- Local type inferenceACM Transactions on Programming Languages and Systems, 2000
- Semi-Explicit First-Class Polymorphism for MLInformation and Computation, 1999
- Putting type annotations to workPublished by Association for Computing Machinery (ACM) ,1996
- Type inference with simple subtypesJournal of Functional Programming, 1991
- Abstract types have existential typeACM Transactions on Programming Languages and Systems, 1988