# A mathematical (categorical) description of type classes

A functional language can be viewed as a category where its objects are types and morphisms functions between them.

How do type classes fit in this model?

I assume we should only consider those implementations that satisfy the constraint that most type-classes have, but that are not expressed in Haskell. For example, we should only consider those implementations of Functor for which fmap id ≡ id and fmap f . fmap g ≡ fmap (f . g).

Or are there any other theoretical foundations for type classes (for example based on typed lambda calculi)?

• You might want to be more explicit about exactly what you want a model for. If you want something that can rigorously describe the open world assumption, the behavior of instance resolution, the interaction of various GHC extensions, &c., that's rather more complicated than an idealized version. Similarly, note that bottoms are often ignored when discussing Hask. – C. A. McCann Sep 6 '12 at 17:08
• Type classes can be thought of as signatures (in the universal algebra sense). The collection of all entities sharing the same signature (elements of the same type class) is a variety. – Dave Clarke Sep 6 '12 at 17:53
• @DaveClarke: It's not immediately obvious to me how to describe type classes on higher kinds that way, but I'm not terribly familiar with universal algebra and might be misunderstanding the correspondence you have in mind... – C. A. McCann Sep 6 '12 at 18:43
• @camccann: I'm not sure how far the correspondence goes. It certainly seemed like a good starting point. – Dave Clarke Sep 6 '12 at 19:16
• @camccann: Just change the base category over which you are defining your algebra: basic type classes like num are signatures over the category of haskell types (or objects of the Hsk category), type classes over type constructors are algebras over the category of functors from Hask to Hask. Note that universal algebra is completely subsumed by the notion of algebra in category theory. Also: Dave: you should turn your comment into an answer. – cody Sep 6 '12 at 19:43

How do type classes fit in this model?

The short answer is: they don't.

Whenever you introduce coercions, type classes, or other mechanisms for ad-hoc polymorphism into a language, the main design issue you face is coherence.

Basically, you need to ensure that typeclass resolution is deterministic, so that a well-typed program has a single interpretation. For example, if you could give multiple instances for the same type in the same scope, you could potentially write ambiguous programs like this:

class Blah a where
blah : a -> String

instance Blah T where
blah _ = "Hello"

instance Blah T where
blah _ = "Goodbye"

v :: T = ...

main :: IO ()
main = print (blah v)  -- does this print "Hello" or "Goodbye"?


Depending on the choice of instance the compiler makes, blah v could equal either "Hello" or "Goodbye". Therefore, the meaning of a program would not be completely determined by the syntax of the program, but rather could be influenced by arbitrary choices the compiler makes.

Haskell's solution to this problem is to require that each type has at most one instance for each typeclass. To ensure this, it permits instance declarations only at the top level, and furthermore makes all declarations globally visible. That way, the compiler can always signal an error if an ambiguous instance declaration is made.

However, making declarations globally visible breaks the compositionality of the semantics. What you can do to recover is to give an elaboration semantics for the programming language -- that is, you can show how to translate Haskell programs into a better-behaved, more compositional language.

This actually gives you a way to compile typeclasses, as well -- it's usually called the "evidence translation" or "dictionary-passing transformation" in Haskell circles, and is one of the early stages of most Haskell compilers.

Typeclasses are also a good example of how programming language design differs from pure type theory. Typeclasses are a really awesome language feature, but they're quite ill-behaved from a proof-theoretic point of view. (This is why Agda does not have typeclasses at all, and why Coq makes them part of its heuristic inference infrastructure.)

• what is the runner up candidate that does have denotational semantics iyswim? – Ohad Kammar Sep 13 '12 at 10:04
• I have no idea, alas. – Neel Krishnaswami Sep 14 '12 at 7:08
• Does this merit an additional question? – Ohad Kammar Sep 14 '12 at 11:27
• @NeelKrishnaswami: Do you have any idea how ML modules fit into this? And what about Agda modules (which someone mentioned to me are "first class")? – Lii Jun 5 '13 at 13:16
• @Lii: ML modules and Agda records are much better-behaved, but it's too complicated to explain in a comment -- ask a question about them, and I (or someone else) will explain. – Neel Krishnaswami Jun 6 '13 at 8:34