Type Inference with Rank 1 Polymorphism for Type-Directed Compilation of ML

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 the 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 typedirected 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 runtime type-passi...

• Type: Conference
• Year: 1999
• Where: ICFP
• Authors: Atsushi Ohori, Nobuaki Yoshida
• Keywords: ICFP 1999, Polymorphic Types, Programming Languages, Type Inference Algorithm, Type System