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

25 August 2003

proceedings article
Published by Association for Computing Machinery (ACM)

Vol. 38 (9) , 39-50
https://doi.org/10.1145/944705.944710

Abstract

We propose a conservative extension of HM(), 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.

Keywords

This publication has 13 references indexed in Scilit:

An extension of HM(X) with bounded existential and universal data-types
Published by Association for Computing Machinery (ACM) ,2003
ML ^F
Published by Association for Computing Machinery (ACM) ,2003
Subtype inequalities
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2003
Information flow inference for ML
ACM Transactions on Programming Languages and Systems, 2003
Colored local type inference
ACM SIGPLAN Notices, 2001
Local type inference
ACM Transactions on Programming Languages and Systems, 2000
Semi-Explicit First-Class Polymorphism for ML
Information and Computation, 1999
Putting type annotations to work
Published by Association for Computing Machinery (ACM) ,1996
Type inference with simple subtypes
Journal of Functional Programming, 1991
Abstract types have existential type
ACM Transactions on Programming Languages and Systems, 1988