Type inference with rank 1 polymorphism for type-directed compilation of ML
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 frdm 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.
References
[1]
K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In Proe. international Conference on Functional Programming, 1998.
[2]
L. Damas and R. Milner. Principal type-schemes for functional programs. Ill Proc. A CM Symposium on Principles of Programming Languages, }pages 207-212, 1982.
[3]
R. Di Cosmo. Deciding type isomorphisms in a typeassignment framework. Journal of Functional Programming, 3(4), 485-525 1993.
[4]
J.-Y. Girard. Une extension de l'interpretation de gSdel ~ l'analyse, et son application ~ l',~limination des coupures dans l'analyse et th6orie des types. In Second Scandinavian Logic Symposium. North-Holland, 1971.
[5]
S. Gorn. Explicit definitions and linguistic dominoes. In J. Hart and S. Takasu, editors, Systems and Computer Science, pages 77-105. University of Toronto Press, 1967.
[6]
R. Harper and J. C. Mitchell. On the type structure of Standard ML. A CM Transactions on Programming Languages and Systems, 15(2):211-252, 1993.
[7]
R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proc. A CM Symposium or~ Principles of Programming Languages, 1995.
[8]
T. Jim. What are principal typings and what are they good for? In Proc. A CM Symposium on Principles of Programming Languages, 1996.
[9]
P. Kanellakis, H.G. Mairson, and J. Mitchell. Unification and ML type reconstruction. In J~L Lassez and G. Plotkin, editors, Computational Logic: Essays in Honor of Alan Robinson. MIT Press, 1990.
[10]
A.J. Kfoury. Type reconstruction in finite rank fragments of the second-order A-calculus. Information and Computation, 15(2):228-257, 1992.
[11]
A.J. Kfoury and J. Wells. A direct algorithm for type inference in the rank 2 fragment of the second-order lambda-calculus. In Proc. A CM Symposium on Principles of Programming Languages, pages 196-207, 1994.
[12]
X. Leroy. The Objective Carol User's Manual. IN- RIA Rocquencourt, B.P. 105 78153 Le Chesnay France, 1997.
[13]
R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.
[14]
R. Milner, R. Tofte, M. Harper, and D. MacQueen. The Definition of Standard ML. The MIT Press, revised edition, 1997.
[15]
Y. Minamide. Compilation based on a calculus for explicit type passing. In Proceedings of Fuji International Workshop on Functional and Logic Programming, pages 301-320, 1996.
[16]
A. Ohori. A polymorphic record calculus and its compilation. A CM Transactions on Programming Languages and Systems, 17(6):844-895, 1995. A preliminary summary appeared at ACM POPL, 1992 under the title "A compilation method for ML-style polymorphic record calculi".
[17]
A. Ohori. Type-directed specialization of polymorphism. Journal of Information and Computation, 1999. To appear. A preliminary summary appeared in Proc. International Conference on Theoretical Aspects of Computer Software, Springer LNCS 1281, pages 107- 137.
[18]
A. Ohori and T. Takamizawa. A polymorphic unboxed calculus as an abstract machine for polymorphic languages. Journal of Lisp and Symbolic Computation, 10(1):61-91, 1997.
[19]
J. Peterson and M. Jones. Implementing type classes. In Proc. A CM Conference on Programming Language Design and Implementation, 1993.
[20]
J.C. Reynolds. Towards a theory of type structure. In Paris Colloq. on Programming, pages 408-425. Springer-Verlag, 1974.
[21]
B. Saha and Z. Shao. Optimal type lifting. In Proc. Types in Compilation, LNCS 1~73, pages 156-177, 1998.
[22]
Z. Shao. Typed common intermediate format. In USENIX Conference on Domain-Specific Languages, 1997.
[23]
D. Tarditi, G. Morrisett, P Cheng, C. Stone, R. Harper, and P. Lee. TIL: A type-directed optimizing compiler for ML. In A CM Conference on Programming Language Design and Implementation, 1996.
[24]
A Tolmach. Tag-free garbage collection using explicit type parameters. In Proc. A CM Conference on Lisp and Functional Programming, 1994.
[25]
A. Wright. Simple imperative polymorphism. Journal of Lisp and Symbolic Computation, 8(4):343-355, 1995.
Index Terms
- Type inference with rank 1 polymorphism for type-directed compilation of ML
Recommendations
Type inference with rank 1 polymorphism for type-directed compilation of ML
ICFP '99: Proceedings of the fourth ACM SIGPLAN international conference on Functional programmingThis paper defines an extended polymorphic type system for an ML-style programming language, and develops a sound and complete type inference algorithm. Different frdm the conventional ML type discipline, the proposed type system allows full rank 1 ...
Finitary polymorphism for optimizing type-directed compilation
We develop a type-theoretical method for optimizing type directed compilation of polymorphic languages, implement the method in SML#, which is a full-scale compiler of Standard ML extended with several advanced features that require type-passing ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sept. 1999
283 pages
Copyright © 1999 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 September 1999
Published in SIGPLAN Volume 34, Issue 9
Check for updates
Qualifiers
- Article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations4Total Citations
- 533Total Downloads
- Downloads (Last 12 months)111
- Downloads (Last 6 weeks)24
Reflects downloads up to 09 Feb 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in