Mark P. Jones
ABSTRACT
Languages like ML and Haskell encourage the view of values as first-class entities that can be passed as arguments or results of functions, or stored as components of data structures. The same languages offer parametric polymorphism, which allows the use of values that behave uniformly over a range of different types. But the combination of these features is not supported-- polymorphic values are not first-class. This restriction is sometimes attributed to the dependence of such languages on type inference, in contrast to more expressive, explicitly typed languages, like System F, that do support first-class polymorphism.This paper uses relationships between types and logic to develop a type system, FCP, that supports first-class polymorphism, type inference, and also first-class abstract datatypes. The immediate result is a more expressive language, but there are also long term implications for language design.
- 1.H.J. Boehm. Partial polymorphic type inference is undeeidable. In #6th Annual Symposium on Foundations of Computer Science, pages 339-345. IEEE, October 1985.Google Scholar
- 2.L. Duponeheel and E. Meijer. On the expressive power of constructor classes. In Proceedings of the 199# Glasgow Functional Programming Workshop, Ayr, September 1994.Google Scholar
- 3.A. Gill, J. Launehbury, and S. L. Peyton Jones. A Short cut to deforestation. In FPCA '93: Conference on Functional Programming Languages and Computer Architecture, Copenhaoen, Denmark, New York, June 1993. ACM Press. Google ScholarDigital Library
- 4.J.-Y. Girard. Une extension de l'interpr#tation de G#Sdel # l'analyse et son application # l'#limination des coupures dans l'analyse et la th#orie de types. In Fenstad, editor, Proceedings of the Scandanavian logic symposium. North Holland, 1971.Google ScholarCross Ref
- 5.C. Hall, K. Hammond, W. Partain, S. Peyton Jones, and P. Wadler. The Glasgow Haskell compihr: a retrospective. In Proceedings of the 1992 Glasgow Workshop on Functional Programming, A yr, Scotland, July 1992. Springer Verlag Workshops in computing series. Google ScholarDigital Library
- 6.It. ttindley. The principal type-scheme of an object in eombinatory logic. Transactions of the American Mathematical Society, 146:29-60, December 1969.Google Scholar
- 7.W. Howard. The formulas-as-types notion of construetion. In To H.B. Curry: Essays on Combinatory Logic, Lambda.Calculus and Formalism, pages 479-490. Academic Press, 1980.Google Scholar
- 8.P. Hudak, S. Peyton Jones, and P. Wadler (editors). Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.2). A CM SIGPLAN Notices, 27(5), May 1992. Google ScholarDigital Library
- 9.P. Hudak and P. Wadler (editors). Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.0). Technical report, University of Glasgow, April 1990.Google Scholar
- 10.M. P. Jones. The implementation of the Gofer functional programming system. Research Report YALEU/DCS/RR-1030, Yale University, New Haven, Connecticut, USA, May 1994.Google Scholar
- 11.M. P. Jones. A system of constructor classes" overloading and implicit higher-order polymorphism. Journal of Functional Programming, 5(1), January 1995 .. #Google ScholarCross Ref
- 12.M. P. Jones. Hugs 1.3 user manual. Technical Report NOTTCS-TR-96;2, Department of Computer Science, University of Nottingham, August 1996.Google Scholar
- 13.S. Kaes. Parametric overloading in polymorphic programming languages. In BSOP '88: European Symposium on Programmingi Nancy, France, New York, 1988. Springer-Verlag. Lecture Notes in Computer Science, 300. . Google ScholarDigital Library
- 14.K. L#iufer. Polymorphic Type Inference and Abstract Data Types. PhD thesis, New York University, July 1992.Google Scholar
- 15.K. L#iufer. Type classes with existential types. Journal of Functional Programming, 6(3):485-517, May 1996,Google ScholarCross Ref
- 16.K. L#iufer and :M' Odersky. Polymorphie type inference and abstract data types. A#CM Trans. actions on Programming Languages and Systems, 16(5)" 1411-1430, September 1994. Google ScholarDigital Library
- 17.J, Launchbury and S. P. Jones. Lazy functional State threads. In Conference on Programming Lang nageDesi#nand: Implementation, Orlando, FL, June 1994: Google ScholarDigital Library
- 18.S. Liang, P. Hua k, M. Jo#, Monad transformers and modular interpreters. In Conferenee record of POPL '95: #nd A6'M S1GPLAN- SIGACT Symposium on Principles of Programming Languages, San FrancisCo, California, January 1995. Google ScholarDigital Library
- 19.R. Milner, A theory of type polymorphism in programming. Journal of Comput;er and-System Sci. ences, 17(3), 1978.Google Scholar
- 20.R. Milner, M'Tofte, and R. Harper. The definition of Standard ML. The MITPress, 1990. Google ScholarDigital Library
- 21.J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. A CM Transactions on Programming Languages and Systems, 10(3):470-502, July 1988. Google ScholarDigital Library
- 22.M. Odersky and K. L#ufer. Putting type annotations to work. In Conference record of POPL '96: 23rd A CM SIGPLAN-SIGA CT Symposium on Principles of Programming Languages, pages 54"67, St, Petersburg Beach, FL, January 1996. ACM press. Google ScholarDigital Library
- 23.N. Perry. The implementation #:of practical func. tional programming languages. PhD thesis, Impe- #rial College, 1991.Google Scholar
- 24.J. Peterson and K. Hammond (editors)., Report on the Programming Language Haskell, A Nonstrict Purely Functional Language (Version 1.0). Research Report YALEU/DCS/RR-1106, Department of Computer Science, Yale University, May 1996.Google Scholar
- 25.S. Peyton Jones. The implementation of functional programming languages. Prentice Hall, 1987. Google ScholarDigital Library
- 26.F. Pfenning, On the undecidability of partial polymorphie type reconstruction. Fundamenta Informatieae, 19(1,2):185-199, 1993. Google ScholarDigital Library
- 27.B' C. Pierce and D. N. Turner. Simple typetheoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207-247, April 1994. : ...Google ScholarCross Ref
- 28.D; R#my. Programming objects: withML, 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 LNCS, pages 321-346. Springer-Verlag, April 1994. Google ScholarDigital Library
- 29.J. Reynolds. Towards a theory of type structure. In Paris colloquium on programming, New York, 1974. Springer-Verlag. Lecture Notes in Computer Science, 19. Google ScholarDigital Library
- 30.J. Robinson. A machine-oriented logic based on the resolution principle. Journal Of the Association for Computing Machinery, 12, 1965. Google ScholarDigital Library
- 31.G. L. Steele Jr. Building interpreters by composing monads. InConference record of POPL '94: elst ACM SIGPLAN-SIGACT Symposium# on Principles of Programming LanguageS, pages 472-492, Portland, OR, January 1994. # Google ScholarDigital Library
- 32.P. Wadler. The essence of functional programming (invited talk). In Conference record of the Nineteenth annual A CM SIGPLAN.SIGA CT symposium on Principles of Programming Languages, .pages 1--14, Jan 1992 ... Google ScholarDigital Library
- 33.P. Wadler and S. Blott. How to make ad hoc polymorphism less ad hoc' In Proceedings of 16th A CM Symposium on Principles of Programming Languages, pages 60-76, Jan 1989. Google ScholarDigital Library
- 34.J. B. Wells. Typability and type checking in the second-order ,#-calculus are equivalent and undeeidable, in Ninth Annual IEEE Symposium on Logic in Computer Science, p agesl 176-185, Paris, France, July 1994.Google ScholarCross Ref
Index Terms
- First-class polymorphism with type inference
Recommendations
Type inference, principal typings, and let-polymorphism for first-class mixin modules
Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Type inference, principal typings, and let-polymorphism for first-class mixin modules
ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programmingA mixin module is a programming abstraction that simultaneously generalizes λ-abstractions, records, and mutually recursive definitions. Although various mixin module type systems have been developed, no one has investigated principal typings or ...
Comments