Semantics of type classes revisited

ABSTRACT

We present a new approach to the semantics of languages with ML-like polymorphic types and type classes. The goals of the new approach are simplicity and generality. Our typing rules are a relatively straightforward extension of the rules for translating core-ML to core-XML. The new features are an encoding of classes as recursive sets of types, and class-membership constraints on types. We show that the soundness of this type of system is independent of the fixedpoint operator used to interpret (recursive) classes, and thus there is no room to engineer a sound notion of well-typing based on other considerations such as decidability. These ideas are applied to investigate the appropriateness of Haskell-style type inference which uses backward chaining for inference of instance relationships. Haskell's algorithm turns out to imply a least fixed point semantics for classes. We show that the Haskell approach is correct and complete for the special case of convergent classes. Although this includes all classes definable in Haskell, most proper extensions of Haskell allow classes that are not convergent, which helps explain the negative results for decidability of type inference for many extensions.

REFERENCES

• 1: Alexander Aiken and Edward L. Wimmers. Solving systems of set constraints. In Proceedings of Seventh LICS Symposium. IEEE Computer Society Press, 1992.
• 2: Stephen Blott. Type Classes. PhD thesis, University of Glasgow, 1991.
• 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: P. Hudak, S. Peyton Jones, and P. Wadler (editors). Report on the Programming Language Haskell, A Non-strict Purely Functional Language (Version 1.1). Technical Report YALEU/DCS/RR777, Yale University, Department of Computer Science, August 1991.
• 5: Mark Jones. Efficient implementation of type class overloading. Manuscript, March 1992.
• 6: Mark P. Jones, A theory of qualified types, Symposium proceedings on 4th European symposium on programming, p.287-306, January 1992, Rennes, France
• 7: Mark Philip Jones, Qualified types: theory and practice (ordering relation), 1992
• 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: A. Kfoury , J. Tiuryn , P. Urzyczyn, Computational consequences and partial solutions of a generalized unification problem, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.98-105, June 1989, Pacific Grove, California, United States
• 10: David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
• 11: J. C. Mitchell , R. Harper, The essence of ML, Proceedings of the 15th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.28-46, January 10-13, 1988, San Diego, California, United States [doi>10.1145/73560.73563]
• 12: 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]
• 13: 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
• 14: W.A. Sutherland. Introduction to Metric and Topological Spaces. Oxford University Press, 1975.
• 15: Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5:285-309, 1955.
• 16: Satish R. Thattd. A simple notion of multiparameter classes with an undecidable type reconstruction problem. Unpublished note (available upon request), 1993.
• 17: 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
• 18: 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; Semantics
      D.3.2 Language Classifications

          Nouns: Haskell

General Terms:
Algorithms, Languages, Theory