Title: A parametric extension of Haskell's type classes
Abstract: Haskell's type classes permit the definition of overloaded operators in a rigorous and general manner that integrate well with the underlying Hindley-Milner type system. As a result, operators that are monomorphic in other typed languages can be given a more general type. Most notably missing in Haskell, however, are overloaded functions over container structures. Such overloaded functions are quite useful, but the current Haskell type system is not expressive enough to support them.
This thesis introduces the notion of parametric type classes and a new type system as a significant generalization of Haskell's type classes. A parametric type class is a class that has type parameters in addition to the placeholder variable which is always present in a class declaration. Haskell's type classes are special instances of parametric type classes with just a placeholder but no parameters. We show that this generalization is essential to representing container structures with overloaded data constructor and selector operations.
The underlying type system supporting our proposed generalization is a version of the Hindley-Milner type system, extended to include a form of constrained quantification. In the extended system, type classes act as constraints on the quantification and instantiation of type variables. This is achieved by putting class constraints on quantified type variables and adding a separate constraint inference sub-system to the standard type inference engine. We prove that the resulting type system is decidable, and provide an effective type inference algorithm to compute the principal types for well-typed terms.
The meaning of a program in our system is described by translating the program, based on its typing derivation, to a program defined in a language that includes constructs for manipulating overloading explicitly. We present a method for extending the type inference algorithm to perform the translation and prove that the resulting algorithm computes the principal translations for well-typed terms. Furthermore, since interpretations of well-typed expressions follow the typing derivations and an expression can be type-checked in more than one way, it is necessary to ensure the coherence of this translation scheme. This is accomplished by defining the corresponding coherence conditions.
Publication Year: 1994
Publication Date: 1994-12-15
Language: en
Type: article
Access and Citation
Cited By Count: 4
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot