Type checking type classes

ABSTRACT

We study the type inference problem for a system with type classes as in the functional programming language Haskell. Type classes are an extension of ML-style polymorphism with overloading. We generalize Milner's work on polymorphism by introducing a separate context constraining the type variables in a typing judgement. This lead to simple type inference systems and algorithms which closely resemble those for ML. In particular we present a new unification algorithm which is an extension of syntactic unification with constraint solving. The existence of principal types follows from an analysis of this unification algorithm.

REFERENCES

• 1: S. Blott. An approach to overloading with polymorphism. PhD thesis, Dept. of Computing Science, University of Glasgow, 1992.
• 2: R. M. Burstall , D. B. MacQueen , D. T. Sannella, HOPE: An experimental applicative language, Proceedings of the 1980 ACM conference on LISP and functional programming, p.136-143, August 25-27, 1980, Stanford University, California, United States [doi>10.1145/800087.802799]
• 3: Kung Chen , Paul Hudak , Martin Odersky, Parametric type classes, Proceedings of the 1992 ACM conference on LISP and functional programming, p.170-181, June 22-24, 1992, San Francisco, California, United States
• 4: Dominique Clément , Thierry Despeyroux , Gilles Kahn , Joëlle Despeyroux, A simple applicative language: mini-ML, Proceedings of the 1986 ACM conference on LISP and functional programming, p.13-27, August 1986, Cambridge, Massachusetts, United States [doi>10.1145/319838.319847]
• 5: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 6: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• 7: Mark P. Jones, A theory of qualified types, Symposium proceedings on 4th European symposium on programming, p.287-306, January 1992, Rennes, France
• 8: Stefan Kaes, Parametric Overloading in Polymorphic Programming Languages, Proceedings of the 2nd European Symposium on Programming, p.131-144, March 21-24, 1988
• 9: 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
• 10: R. Milner. A theory of type polymorphism in programming. J. Comp. Sys. Sci., 17:348-375, 1978.
• 11: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 12: 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
• 13: Dennis M. Volpano , Geoffrey S. Smith, On the complexity of ML typeability with overloading, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.15-28, June 1991, Cambridge, Massachusetts, United States
• 14: 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]

INDEX TERMS

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

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax
      D.3.2 Language Classifications

          Nouns: Haskell
      D.3.3 Language Constructs and Features
          Subjects: Procedures, functions, and subroutines

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

General Terms:
Algorithms, Languages, Theory, Verification