Article

Type classes with more higher-order polymorphism

Authors:

Matthias Neubauer,

Peter ThiemannAuthors Info & Claims

ICFP '02: Proceedings of the seventh ACM SIGPLAN international conference on Functional programming

Pages 179 - 190

https://doi.org/10.1145/581478.581496

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.]]

Digital Library

[5]

D. Duggan, G. V. Cormack, and J. Ophel. Kinded type inference for parametric overloading. Acta Inf., 33(1):21--68, 1996.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[13]

M. P. Jones. Qualified Types: Theory and Practice. Cambridge University Press, Cambridge, UK, 1994.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[24]

J. Mitchell. Foundations for Programming Languages. MIT Press, 1996.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[35]

C. Prehofer. Decidable higher-order unification problems. In Automated Deduction CADE-12, 12th International Conference on Automated Deduction. Springer, 1994.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

[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.]]

Digital Library

Cited By

Alkemade TJeuring J(2015)Type Class Instances for Type-Level Lambdas in HaskellRevised Selected Papers of the 16th International Symposium on Trends in Functional Programming - Volume 954710.1007/978-3-319-39110-6_4(60-84)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1007/978-3-319-39110-6_4
Eisenberg RWeirich S(2012)Dependently typed programming with singletonsACM SIGPLAN Notices10.1145/2430532.236452247:12(117-130)Online publication date: 13-Sep-2012
https://dl.acm.org/doi/10.1145/2430532.2364522
Eisenberg RWeirich SVoigtländer J(2012)Dependently typed programming with singletonsProceedings of the 2012 Haskell Symposium10.1145/2364506.2364522(117-130)Online publication date: 13-Sep-2012
https://dl.acm.org/doi/10.1145/2364506.2364522
Show More Cited By

Index Terms

Type classes with more higher-order polymorphism
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Polymorphism
      2. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Type classes with more higher-order polymorphism

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 ...
Type Class Instances for Type-Level Lambdas in Haskell
TFP 2015: Revised Selected Papers of the 16th International Symposium on Trends in Functional Programming - Volume 9547

Haskell 2010 lacks flexibility in creating instances of type classes for type constructors with multiple type arguments. We would like to make the order of type arguments to a type constructor irrelevant to how type class instances can be specified. ...
Bidirectional type class instances
Haskell 2019: Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell

GADTs were introduced in Haskell’s eco-system more than a decade ago, but their interaction with several mainstream features such as type classes and functional dependencies has a lot of room for improvement. More specifically, for some GADTs it can be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

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

Conference Chair:
Mitchell Wand
Northeastern University
,
Program Chair:
Simon Peyton Jones
Microsoft Research Ltd., Cambridge

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

Copyright © 2002 ACM.

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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 17 September 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

ICFP02

Sponsor:

ICFP02: International Conference on Functional Programming

October 4 - 6, 2002

PA, Pittsburgh, USA

Acceptance Rates

ICFP '02 Paper Acceptance Rate 24 of 76 submissions, 32%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
441
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Oct 2024

Other Metrics

View Author Metrics

Citations

Cited By

Alkemade TJeuring J(2015)Type Class Instances for Type-Level Lambdas in HaskellRevised Selected Papers of the 16th International Symposium on Trends in Functional Programming - Volume 954710.1007/978-3-319-39110-6_4(60-84)Online publication date: 3-Jun-2015
https://dl.acm.org/doi/10.1007/978-3-319-39110-6_4
Eisenberg RWeirich S(2012)Dependently typed programming with singletonsACM SIGPLAN Notices10.1145/2430532.236452247:12(117-130)Online publication date: 13-Sep-2012
https://dl.acm.org/doi/10.1145/2430532.2364522
Eisenberg RWeirich SVoigtländer J(2012)Dependently typed programming with singletonsProceedings of the 2012 Haskell Symposium10.1145/2364506.2364522(117-130)Online publication date: 13-Sep-2012
https://dl.acm.org/doi/10.1145/2364506.2364522
Chakravarty MKeller GJones S(2005)Associated type synonymsACM SIGPLAN Notices10.1145/1090189.108639740:9(241-253)Online publication date: 12-Sep-2005
https://dl.acm.org/doi/10.1145/1090189.1086397
Chakravarty MKeller GJones SDanvy OPierce B(2005)Associated type synonymsProceedings of the tenth ACM SIGPLAN international conference on Functional programming10.1145/1086365.1086397(241-253)Online publication date: 28-Sep-2005
https://dl.acm.org/doi/10.1145/1086365.1086397
Abel AMatthes RUustalu T(2005)Iteration and coiteration schemes for higher-order and nested datatypesTheoretical Computer Science10.1016/j.tcs.2004.10.017333:1-2(3-66)Online publication date: 1-Mar-2005
https://dl.acm.org/doi/10.1016/j.tcs.2004.10.017
Thiemann P(2002)Programmable Type Systems for Domain Specific LanguagesElectronic Notes in Theoretical Computer Science10.1016/S1571-0661(04)80796-576(233-251)Online publication date: Nov-2002
https://doi.org/10.1016/S1571-0661(04)80796-5

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents