Atsushi Ohori
Nobuaki Yoshida
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.
- 1.K. Crary, S. Weirich, and G. Morrisett. Intensional polymorphism in type-erasure semantics. In Proe. international Conference on Functional Programming, 1998. Google Scholar
Digital Library
- 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. Google ScholarDigital Library
- 3.R. Di Cosmo. Deciding type isomorphisms in a typeassignment framework. Journal of Functional Programming, 3(4), 485-525 1993.Google ScholarCross Ref
- 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.Google ScholarCross Ref
- 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.Google Scholar
- 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. Google ScholarDigital Library
- 7.R. Harper and G. Morrisett. Compiling polymorphism using intensional type analysis. In Proc. A CM Symposium or~ Principles of Programming Languages, 1995. Google ScholarDigital Library
- 8.T. Jim. What are principal typings and what are they good for? In Proc. A CM Symposium on Principles of Programming Languages, 1996. Google ScholarDigital Library
- 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.Google Scholar
- 10.A.J. Kfoury. Type reconstruction in finite rank fragments of the second-order A-calculus. Information and Computation, 15(2):228-257, 1992. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 12.X. Leroy. The Objective Carol User's Manual. IN- RIA Rocquencourt, B.P. 105 78153 Le Chesnay France, 1997.Google Scholar
- 13.R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, 1978.Google ScholarCross Ref
- 14.R. Milner, R. Tofte, M. Harper, and D. MacQueen. The Definition of Standard ML. The MIT Press, revised edition, 1997. Google ScholarDigital Library
- 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.Google Scholar
- 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". Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 19.J. Peterson and M. Jones. Implementing type classes. In Proc. A CM Conference on Programming Language Design and Implementation, 1993. Google ScholarDigital Library
- 20.J.C. Reynolds. Towards a theory of type structure. In Paris Colloq. on Programming, pages 408-425. Springer-Verlag, 1974. Google ScholarDigital Library
- 21.B. Saha and Z. Shao. Optimal type lifting. In Proc. Types in Compilation, LNCS 1~73, pages 156-177, 1998. Google ScholarDigital Library
- 22.Z. Shao. Typed common intermediate format. In USENIX Conference on Domain-Specific Languages, 1997. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 24.A Tolmach. Tag-free garbage collection using explicit type parameters. In Proc. A CM Conference on Lisp and Functional Programming, 1994. Google ScholarDigital Library
- 25.A. Wright. Simple imperative polymorphism. Journal of Lisp and Symbolic Computation, 8(4):343-355, 1995. Google ScholarDigital Library
Index Terms
- Type inference with rank 1 polymorphism for type-directed compilation of ML
Recommendations
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 ...
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 frdm the conventional ML type discipline, the proposed type system allows full rank 1 ...
Comments