Nothing Special   »   [go: up one dir, main page]

skip to main content
article

Type classes with more higher-order polymorphism

Published: 17 September 2002 Publication History

Abstract

We propose an extension of Haskell's type class system with lambda abstractions in the type language. Type inference for our extension relies on a novel constrained unification procedure called guided higher-order unification. This unification procedure is more general than Haskell's kind-preserving unification but less powerful than full higher-order unification.The main technical result is the soundness and completeness of the unification rules for the fragment of lambda calculus that we admit on the type level.

References

[1]
H. P. Barendregt. The Lambda Calculus --- Its Syntax and Semantics. North-Holland, 1984.]]
[2]
G. Dowek. A second order pattern matching algorithm in the cube of typed λ-calculi. In Proceedings of Mathematical Fundation of Computer Science Lecture Notes in Computer Science 520, pages 151--160, 1991. Rapport de Recherche 1585, INRIA, 1992.]]
[3]
G. Dowek. Third order matching is decidable. In Proceedings of the 1992 IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1992.]]
[4]
G. Dowek. Higher-order unification and matching. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume 2, chapter 16, pages 1009--1062. North-Holland, 2001.]]
[5]
D. Duggan, G. V. Cormack, and J. Ophel. Kinded type inference for parametric overloading. Acta Inf., 33(1):21--68, 1996.]]
[6]
W. M. Farmer. A unification algorithm for second-order monadic terms. Annals of Pure and Applied Logic, 39:131--174, 1988.]]
[7]
W. M. Farmer. Simple second-order languages for which unification is undecidable. Theoretical Comput. Sci., 87(1):25--41, Sept. 1991.]]
[8]
W. D. Goldfarb. The undecidability of the second-order unification problem. Theoretical Comput. Sci., 13(2):225--230, Feb. 1981.]]
[9]
Haskell 98, a non-strict, purely functional language. http://www.haskell.org/definition, Dec. 1998.]]
[10]
J. R. Hindley. The principal type scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29--60, 1969.]]
[11]
G. Huet. A unification algorithm for typed λ-calculus. Theoretical Comput. Sci., 1(1):27--57, 1975.]]
[12]
M. P. Jones. A system of constructor classes: Overloading and implicit higher-order polymorphism. In Arvind, editor, Proc. Functional Programming Languages and Computer Architecture 1993, pages 52--61, Copenhagen, Denmark, June 1993. ACM Press, New York.]]
[13]
M. P. Jones. Qualified Types: Theory and Practice. Cambridge University Press, Cambridge, UK, 1994.]]
[14]
M. P. Jones. Functional programming with overloading and higher-order polymorphism. In Advanced Functional Programming, volume 925 of Lecture Notes in Computer Science, pages 97--136. Springer-Verlag, May 1995.]]
[15]
M. P. Jones. Simplifying and improving qualified types. In S. Peyton Jones, editor, Proc. Functional Programming Languages and Computer Architecture 1995, pages 160--169, La Jolla, CA, June 1995. ACM Press, New York.]]
[16]
M. P. Jones. Typing Haskell in Haskell. In E. Meijer, editor, Proceedings of the 1999 Haskell Workshop, number UU-CS-1999-28 in Technical Reports, 1999. ftp://ftp.cs.uu.nl/pub/RUU/CS/techreps/CS-1999/1999-28.pdf.]]
[17]
M. P. Jones. Type classes with functional dependencies. In G. Smolka, editor, Proc. 9th European Symposium on Programming, number 1782 in Lecture Notes in Computer Science, pages 230--244, Berlin, Germany, Mar. 2000. Springer-Verlag.]]
[18]
S. Kaes. Parametric overloading in polymorphic programming languages. In H. Ganzinger, editor, Proc. 2nd European Symposium on Programming 1988, number 300 in Lecture Notes in Computer Science, pages 131--144. Springer-Verlag, 1988.]]
[19]
S. Kaes. Type inference in the presence of overloading, subtyping and recursive types. In Proc. 1992 ACM Conference on Lisp and Functional Programming, page x, San Francisco, California, USA, June 1992.]]
[20]
D. Miller. Unification of simply typed lambda-terms as logic programming. In K. Furukawa, editor, Eighth International Logic Programming Conference, pages 255--269, Paris, France, June 1991. MIT Press.]]
[21]
D. Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321--358, Oct. 1992.]]
[22]
R. Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17:348--375, 1978.]]
[23]
R. Milner, M. Tofte, R. Harper, and D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.]]
[24]
J. Mitchell. Foundations for Programming Languages. MIT Press, 1996.]]
[25]
G. Nadathur and D. Miller. An overview of λ PROLOG. In R. A. Kowalski and K. A. Bowen, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 810--827, Seattle, 1988. ALP, IEEE, The MIT Press.]]
[26]
P. Narendran. Some remarks on second order unification. Technical Report 89/356/18, University of Calgary, July 1989.]]
[27]
T. Nipkow. Functional unification of higher-order patterns. In Proc. of the 8th Annual IEEE Symposium on Logic in Computer Science, pages 64--74. IEEE Computer Society Press, 1993.]]
[28]
T. Nipkow and C. Prehofer. Type checking type classes. In Proceedings of the 1993 ACM SIGPLAN Symposium on Principles of Programming Languages, pages 409--418, Charleston, South Carolina, Jan. 1993. ACM Press.]]
[29]
T. Nipkow and G. Snelting. Type classes and overloading resolution via order-sorted unification. In J. Hughes, editor, Proc. Functional Programming Languages and Computer Architecture 1991, number 523 in Lecture Notes in Computer Science, pages 1--14, Cambridge, MA, 1991. Springer-Verlag.]]
[30]
L. C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and Computer Science, pages 361--385. Academic Press, 1990.]]
[31]
S. Peyton Jones, M. Jones, and E. Meijer. Type classes: An exploration of the design space. In J. Launchbury, editor, Proc. of the Haskell Workshop, Amsterdam, The Netherlands, June 1997. Yale University Research Report YALEU/DCS/RR-1075.]]
[32]
F. Pfenning. Partial polymorphic type inference and higher-order unification. In ACM Conference on Lisp and Functional Programming, pages 153--163, Snowbird, Utah, 1988. ACM Press.]]
[33]
F. Pfenning. Logic programming in the LF logical framework. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 149--181. Cambridge University Press, 1991.]]
[34]
F. Pfenning and C. Schürmann. Algorithms for equality and unification in the presence of notational definitions. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types for Proofs and Programs, number 1657 in Lecture Notes in Computer Science, pages 179--193, Kloster Irsee, Germany, Mar. 1998.]]
[35]
C. Prehofer. Decidable higher-order unification problems. In Automated Deduction CADE-12, 12th International Conference on Automated Deduction. Springer, 1994.]]
[36]
M. Schmidt-SchauΒ and K. U. Schulz. Decidability of bounded higher order unification. Technical Report Frank-15, Universität Frankfurt, 2001.]]
[37]
P. Thiemann. Wash/CGI: Server-side Web scripting with sessions and typed, compositional forms. In Practical Aspects of Declarative Languages, Proceedings of the Fourth International Workshop, PADL'02, number 2257 in Lecture Notes in Computer Science, pages 192--208, Portland, OR, USA, Jan. 2002. Springer-Verlag.]]
[38]
P. Wadler and S. Blott. How to make ad-hoc polymorphism less ad-hoc. In Proc. 16th Annual ACM Symposium on Principles of Programming Languages, pages 60--76, Austin, Texas, Jan. 1989. ACM Press.]]
[39]
Web authoring system in Haskell (WASH). http://www.informatik.uni-freiburg.de/~thiemann/haskell/WASH, Mar. 2001.]]
[40]
D. A. Wolfram. The Clausal Theory of Types. Cambridge tracts in Theoretical Computer Science. Cambridge University Press, 1993.]]

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 37, Issue 9
September 2002
283 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/583852
Issue’s Table of Contents
  • cover image ACM Conferences
    ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming
    October 2002
    294 pages
    ISBN:1581134878
    DOI:10.1145/581478
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: 17 September 2002
Published in SIGPLAN Volume 37, Issue 9

Check for updates

Author Tags

  1. Haskell
  2. higher-order unification
  3. type classes
  4. type inference

Qualifiers

  • Article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)1
  • Downloads (Last 6 weeks)0
Reflects downloads up to 28 Nov 2024

Other Metrics

Citations

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Media

Figures

Other

Tables

Share

Share

Share this Publication link

Share on social media