ML^F: raising ML to the power of system F

Abstract

We propose a type system ML^F that generalizes ML with first-class polymorphism as in System F. Expressions may contain second-order type annotations. Every typable expression admits a principal type, which however depends on type annotations. Principal types capture all other types that can be obtained by implicit type instantiation and they can be inferred.All expressions of ML are well-typed without any annotations. All expressions of System F can be mechanically encoded into ML^F by dropping all type abstractions and type applications, and injecting types of lambda-abstractions into ML^F types. Moreover, only parameters of lambda-abstractions that are used polymorphically need to remain annotated.

References

1. H.-J. Boehm. Partial polymorphic type inference is undecidable. In 26th Annual Symposium on Foundations of Computer Science, pages 339--345. IEEE Computer Society Press, Oct. 1985.
2. L. Cardelli. An implementation of FSub. Research Report 97, Digital Equipment Corporation Systems Research Center, 1993.
3. R. D. Cosmo. Isomorphisms of Types: from lambda-calculus to information retrieval and language design. Birkhauser, 1995.
4. L. Damas and R. Milner. Principal type-schemes for functional programs. In Proceedings of the Ninth ACM Conference on Principles of Programming Langages, pages 207--212, 1982.
5. G. Dowek, T. Hardin, C. Kirchner, and F. Pfenning. Higher-order unification via explicit substitutions: the case of higher-order patterns. In M. Maher, editor, Joint international conference and symposium on logic programming, pages 259--273, 1996.
6. J. Garrigue. Relaxing the value-restriction. Presented at the third Asian workshop on Programmaming Languages and Systems (APLAS), 2002.
7. J. Garrigue and D. Rémy. Extending ML with semi-explicit higher-order polymorphism. Journal of Functional Programming, 155(1/2):134--169, 1999. A preliminary version appeared in TACS'97.
8. The GHC Team. The Glasgow Haskell Compiler User's Guide, Version 5.04, 2002. Chapter Arbitrary-rank polymorphism.
9. P. Giannini and S. R. D. Rocca. Characterization of typings in polymorphic type discipline. In Third annual Symposium on Logic in Computer Science, pages 61--70. IEEE, 1988.
10. J. James William O'Toole and D. K. Gifford. Type reconstruction with first-class polymorphic values. In SIGPLAN '89 Conference on Programming Language Design and Implementation, Portland, Oregon, June 1989. ACM. also in ACM SIGPLAN Notices 24(7), July 1989.
11. T. Jim. Rank-2 type systems and recursive definitions. Technical Report MIT/LCS/TM-531, Massachusetts Institute of Technology, Laboratory for Computer Science, Nov. 1995.
12. T. Jim. What are principal typings and what are they good for? In ACM, editor, ACM Symposium on Principles of Programming Languages (POPL), St. Petersburg Beach, Florida, pages 42--53, 1996.
13. A. J. Kfoury and J. B. Wells. A direct algorithm for type inference in the rank-2 fragment of the second-order lambda -calculus. In ACM Conference on LISP and Functional Programming, 1994.
14. A. J. Kfoury and J. B. Wells. Principality and decidable type inference for finite-rank intersection types. In ACM Symposium on Principles of Programming Languages (POPL), pages 161--174. ACM, Jan. 1999.
15. K. Läufer and M. Odersky. Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Sys-tems, 16(5):1411--1430, Sept. 1994.
16. X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system, documentation and user's manual - release 3.05. Technical report, INRIA, July 2002. Documentation distributed with the Objective Caml system.
17. Mark P Jones, Alastair Reid, the Yale Haskell Group, and the OGI School of Science & Engineering at OHSU. An overview of hugs extensions. Available electronically, 1994--2002.
18. D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321--358, 1992.
19. J. C. Mitchell. Polymorphic type inference and containment. Information and Computation, 2/3(76):211--249, 1988.
20. M. Odersky and K. Läufer. Putting type annotations to work. In Proceedings of the 23rd ACM Conference on Principles of Programming Languages, pages 54--67, Jan. 1996.
21. M. Odersky, C. Zenger, and M. Zenger. Colored local type inference. ACM SIGPLAN Notices, 36(3):41--53, Mar. 2001.
22. F. Pfenning. Partial polymorphic type inference and higher-order unification. In Proceedings of the ACM Conference on Lisp and Functional Programming, pages 153--163. ACM Press, July 1988.
23. F. Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 19(1,2):185--199, 1993. Preliminary version available as Technical Report CMU-CS-92-105, School of Computer Science, Carnegie Mellon University, January 1992.
24. B. C. Pierce and D. N. Turner. Local type inference. In Proceedings of the 25th ACM Conference on Principles of Programming Languages, 1998. Full version in ACM Transactions on Programming Languages and Systems (TOPLAS), 22(1), January 2000, pp. 1--44.
25. D. Rémy. Programming objects with ML-ART: An extension to ML with abstract and record types. In M. Hagiya and J. C. Mitchell, editors, Theoretical Aspects of Computer Software, volume 789 of Lecture Notes in Computer Science, pages 321--346. Springer-Verlag, April 1994.
26. J. B. Wells. Typability and type checking in the second order ?-calculus are equivalent and undecidable. In Ninth annual IEEE Sym-posium on Logic in Computer Science, pages 176--185, July 1994.
27. J. B. Wells. Type Inference for System F with and without the Eta Rule. PhD thesis, Boston University, 1996.
28. A. K. Wright. Simple imperative polymorphism. Lisp and Symbolic Computation, 8(4):343--355, 1995.

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features