Martin Odersky
Konstantin Läufer
ABSTRACT
We study an extension of the Hindley/Milner system with explicit type scheme annotations and type declarations. The system can express polymorphic function arguments, user-defined data types with abstract components, and structure types with polymorphic fields. More generally, all programs of the polymorphic lambda calculus can be encoded by a translation between typing derivations. We show that type reconstruction in this system can be reduced to the decidable problem of first-order unification under a mixed prefix.
- Aug94.L. Augustsson. Haskell B. user's manual version 0.999.7, October 1994. Distributed with the HBC compiler.Google Scholar
- BMS80.Rod Burstall, David MacQueen, and Donald T. Sanella. Hope: An experimental applicative language. In Conference Record of the 1980 LISP Conference, pages 136-143, Redwood Estates, California, August 1980. The LISP Company. Google ScholarDigital Library
- Boe89.Hans-J. Boehm. Type inference in the presence of type abstraction. In Proceedings of the SIGPLAN '89 Conference on Programming Language Design and Implementation, pages 192-206. ACM, ACM Press, June 1989. Google ScholarDigital Library
- DM82.Luis Damas and Robin Milner. Principal type schemes for functional programs. In Proc. 9th A CM Symposium on Principles of Programming Languages, January 1982. Google ScholarDigital Library
- Fel90.Matthias Felleisen. On the expressive power of programming languages. In Neil D. Jones, editor, ESOP '90, European Symposium on Programming, pages 134-151. Springer-Verlag, 1990. Lecture Notes in Computer Science 432. Google ScholarDigital Library
- Gir71.J. Girard. Une extension de l'interpretation de GOdel a l'analyse, et son application a l'elimination des coupures dans l'anMyse et la theorie des types. In 2nd Scandznavian Logic Symp., pages 63-92, 1971.Google ScholarCross Ref
- Hen93.Fritz Henglein. Type inference with polymorphic recursion. A CM Transactions on Programming Languages and Systems, 15(1):253-289, April 1993. Google ScholarDigital Library
- Jon92.Mark P. Jones. Qualified Types: Theory and Pract, ce. D.phil. thesis, Oxford University, September 1992. Google ScholarDigital Library
- Jon95.Mark P. Jones. From Hindley-Milner types to first-class structures. In Proc. Hasketl Workshop, La Jolla, pages 1t5-136, June 1995. Yale University Research Report YALEU/DCS/RR-1075.Google Scholar
- KTU89.A. Kfoury, J. Tiuryn, and P. Urzyczyn. The undecidability of the semi-unification problem. Technical Report BUCS-89-010, Boston University, Oct. 1989. also in Proc. of Symp. on Theory of Computing, Baltimore, Maryland, May 1990. Google ScholarDigital Library
- KTU93.A.J. Kfoury, J. Tiuryn, and P. Urzyczyn. Type reconstruction in the presence of polymorphic recursion. A CM Transactions on Programming Languages and Systems. 15(1):290-311, April 1993. Google ScholarDigital Library
- LMM87.J. Lassez, M. Maher, and K. Marriott. Unification revisited. In J. Minker, editor, Foundations of Deductive Databases and Logic Programming. Morgan Kauffman, 1987. Google ScholarDigital Library
- LO94.Konstantin Litufer and Martin Odersky. Polymorphic type inference and abstract data types. A CM Transactions on Programming Languages and Systems, 16(5):1411-1430, September 1994. Google ScholarDigital Library
- LPar.John Launchbury and Simon Peyton Jones. State in Haskell. Lisp and Symbolic Computation, to appear. Google ScholarDigital Library
- McC84.N. McOracken. The typechecking of programs with implicit type structure. In Gilles Kahn, David B. MacQueen, and Gordon D. Plotkin, editors, Semantics of Data Types, pages 301-315. Springer-Verlag, June 1984. Lecture Notes in Computer Science 173. Google ScholarDigital Library
- Mil78.Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348-375, Dec 1978.Google ScholarCross Ref
- Mil92.Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14:321-358, 1992. Google ScholarDigital Library
- Mit90.John C. Mitchell. Polymorphic type inference and containment, in G6rard Huet, editor, Logical Foundations of Functional Programming, The UT Year of Programming Series, chapter 8. Addison-Wesley Publishing Company, Inc., 1990. Google ScholarDigital Library
- Mor68.J.H. Morris. Lambda-Calculus Models of Programming Languages. PhD thesis, Massachusetts Institute of Technology, 1968. Technical Report MAC-TR-57.Google Scholar
- MP88.J. Mitchell and G. Plotkin. Abstract types have existential types. A CM Trans. on Programming Languages and Systems, 10(3):470-502, 1988. Google ScholarDigital Library
- MP93.M. Mauny and F. Pottier. An implementation of Carol-Light with existential types. Technical report, INRIA, October 1993. Distributed with the Caml-Light system.Google Scholar
- Myc84.A. Mycroft. Polymorphic type schemes and recursive definitions. In Proc. 6th Int. Symposium. on Programming, LNCS 167, 1984. Google ScholarDigital Library
- OG89.James William O'Toole and David K. Gifford. Polymorphic type reconstruction. In Proceedings of the A CM SIGPLAN Conference on Programming Language Design and Implementation, pages 207-217. ACM, ACM Press, June 1989.Google Scholar
- OL95.Martin Odersky and Konstantin Laufer. Type reconstruction in the presence of type scheme annotations. Technical report, University of Karlsruhe, 1995. forthcoming.Google Scholar
- OWW95.Martin Odersky, Philip Wadler, and Martin Wehr. A second look at overloading. In Proc. A CM Conf. on Functional Programming and Computer Architecture, pages 135-1469, June 1995. Google ScholarDigital Library
- Per90.N. Perry. The Implementation of Practical Functional Programming Languages. P hD thesis, Imperial College of Science, Technology, and Medicine, University of London, 1990.Google Scholar
- Pfe88.Frank Pfenning. Partial polymorphic type inference and higher-order unification. In Proceedings of the 1988 A CM Conference on Lisp and Functional Programming, pages 153-163, July 1988. Google ScholarDigital Library
- Rém89.Didier R#my. Typechecking records and variants in a natural extension of ML. In Proc. 16th A CM Symposium on Principles of Programming Languages, 1989. Google ScholarDigital Library
- Rém94.Didier R#my. Programming objects with ML- ART, and extension to ML with abstract and record types. In Proc. Theoretical Aspects of Computer Software, pages 321-346, April 1994. Springer LNCS 789. Google ScholarDigital Library
- Rey74.John C. Reynolds. Towards a theory of type structure. In International Programming Symposium, pages 408-425. Springer-Verlag, 1974. Lecture Notes in Computer Science 19. Google ScholarDigital Library
- Wel94.J.B. Wells. Typability and type checking in the second order h-calculus are equivalent and undecidable. In Proc. 9th IEEE Symposium on Logic in Computer Science, pages 176-185, July 1994.Google ScholarCross Ref
Index Terms
- Putting type annotations to work
Recommendations
Putting Gradual Types to Work
Practical Aspects of Declarative LanguagesAbstractIn this paper, we describe our experience incorporating gradual types in a statically typed functional language with Hindley-Milner style type inference. Where most gradually typed systems aim to improve static checking in a dynamically typed ...
Taming type annotations in gradual typing
Gradual typing provides a methodology to integrate static and dynamic typing, harmonizing their often conflicting advantages in a single language. When a user wants to enjoy the advantages of static typing, most gradual languages require that they add ...
Recursive type generativity
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingExistential types provide a simple and elegant foundation for understanding generative abstract data types, of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found ...
Comments