Type classes with more higher-order polymorphism

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: Gilles Dowek, Higher-order unification and matching, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
• 5: Dominic Duggan , Gordon Cormack , John Ophel, Kinded type inference for parametric overloading, Acta Informatica, v.33 n.1, p.21-68, 1996 [doi>10.1007/s002360050035]
• 6: W. M. Farmer. A unification algorithm for second-order monadic terms. Annals of Pure and Applied Logic, 39:131--174, 1988.
• 7: William M. Farmer, Simple second-order languages for which unification is undecidable, Theoretical Computer Science, v.87 n.1, p.25-41, Sept. 16, 1991 [doi>10.1016/0304-3975(91)90024-V]
• 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: Mark P. Jones, A system of constructor classes: overloading and implicit higher-order polymorphism, Proceedings of the conference on Functional programming languages and computer architecture, p.52-61, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165190]
• 13: Mark P. Jones, Qualified types: theory and practice, Cambridge University Press, New York, NY, 1995
• 14: Mark P. Jones, Functional Programming with Overloading and Higher-Order Polymorphism, Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text, p.97-136, May 24-30, 1995
• 15: Mark P. Jones, Simplifying and improving qualified types, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.160-169, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224198]
• 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: Mark P. Jones, Type Classes with Functional Dependencies, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.230-244, April 02, 2000
• 18: Stefan Kaes, Parametric Overloading in Polymorphic Programming Languages, Proceedings of the 2nd European Symposium on Programming, p.131-144, March 21-24, 1988
• 19: Stefan Kaes, Type inference in the presence of overloading, subtyping and recursive types, Proceedings of the 1992 ACM conference on LISP and functional programming, p.193-204, June 22-24, 1992, San Francisco, California, United States
• 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: Dale Miller, Unification under a mixed prefix, Journal of Symbolic Computation, v.14 n.4, p.321-358, Oct. 1992 [doi>10.1016/0747-7171(92)90011-R]
• 22: R. Milner. A theory of type polymorphism in programming. J. Comput. Syst. Sci., 17:348--375, 1978.
• 23: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 24: John C. Mitchell, Foundations of programming languages, MIT Press, Cambridge, MA, 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: Tobias Nipkow , Christian Prehofer, Type checking type classes, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.409-418, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158698]
• 29: Tobias Nipkow , Gregor Snelting, Type classes and overloading resolution via order-sorted unification, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.1-14, June 1991, Cambridge, Massachusetts, United States
• 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: Frank Pfenning, Partial polymorphic type inference and higher-order unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.153-163, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62697]
• 33: Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 34: Frank Pfenning , Carsten Schürmann, Algorithms for Equality and Unification in the Presence of Notational Definitions, Selected papers from the International Workshop on Types for Proofs and Programs, p.179-193, March 27-31, 1998
• 35: Christian Prehofer, Decidable Higher-Order Unification Problems, Proceedings of the 12th International Conference on Automated Deduction, p.635-649, June 26-July 01, 1994
• 36: M. Schmidt-SchauΒ and K. U. Schulz. Decidability of bounded higher order unification. Technical Report Frank-15, Universität Frankfurt, 2001.
• 37: Peter Thiemann, WASH/CGI: Server-Side Web Scripting with Sessions and Typed, Compositional Forms, Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages, p.192-208, January 19-20, 2002
• 38: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]
• 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 University Press, New York, NY, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
Haskell, higher-order unification, type classes, type inference