A mathematical (categorical) description of type classes
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 -&gt; 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.)