Type inference with rank 1 polymorphism for type-directed compilation of ML

Atsushi Ohori, Nobuaki Yoshida

Research output: Contribution to journalArticlepeer-review

6 Citations (Scopus)

Abstract

This paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different from the conventional ML type discipline, the proposed type system allows full rank 1 polymorphism, where polymorphic types can appear in other types such as product types, disjoint union types and range types of function types. Because of this feature, the proposed type system significantly reduces the value-only restriction of polymorphism, which is currently adopted in most of ML-style impure languages. It also serves as a basis for efficient implementation of type-directed compilation of polymorphism. The extended type system achieves more efficient type inference algorithm, and it also contributes to develop more efficient type-passing implementation of polymorphism. We show that the conventional ML polymorphism sometimes introduces exponential overhead both at compile-time elaboration and run-time type-passing execution, and that these problems can be eliminated by our type inference system. Compared with a more powerful rank 2 type inference systems based on semi-unification, the proposed type inference algorithm infers a most general type for any typable expression by using the conventional first-order unification, and it is therefore easily adopted in existing implementation of ML family of languages.

Original languageEnglish
Pages (from-to)160-171
Number of pages12
JournalSIGPLAN Notices (ACM Special Interest Group on Programming Languages)
Volume34
Issue number9
DOIs
Publication statusPublished - 1999 Sep
Externally publishedYes

ASJC Scopus subject areas

  • Software
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Type inference with rank 1 polymorphism for type-directed compilation of ML'. Together they form a unique fingerprint.

Cite this