Type classes and kinds

Every abstraction of this part (monoid, functor, monad) is expressed in Haskell by a single mechanism — the type class: an overloadable interface plus laws that implementations must obey. A class with laws is an algebraic structure, not merely an interface as in, say, TypeScript.

As an example, consider the Functor type class: the class declaration defines the interface — the signature of the single method $\mathtt{fmap}$ — and an instance declaration implements this interface for a concrete type, here for $\mathtt{Maybe}$.

class Functor f where
  -- fmap applies an ordinary function inside the context f
  fmap :: (a -> b) -> f a -> f b

instance Functor Maybe where
  -- if there is a value, apply the function to it
  fmap g (Just x) = Just (g x)
  -- if there is none, the Nothing context is preserved
  fmap g Nothing = Nothing

A method call is dispatched by type: the compiler sees that $\mathtt{fmap}$ is applied to a value of type $\mathtt{Maybe}$ and picks the instance above. Moreover, a type class can dispatch on the return type as well: for example, $\mathtt{mempty}$ — the neutral element from the Monoid class — takes no arguments at all and “learns” its type from the call site. Class laws are not checked by the compiler — they are a contract on the conscience of the instance author: a class can be instantiated incorrectly — say, with an $\mathtt{fmap}$ that loses elements of the container — the compiler will accept such an instance, but code that relies on the laws will start producing wrong results. One more rule: a type gets at most one instance of a class (coherence).

Now, kinds: a kind tells how many parameters a constructor still lacks to become an ordinary type with values.

Int :: *
-- Int is an ordinary type: it has values

Maybe :: * -> *
-- Maybe is a type constructor with one parameter

Either :: * -> * -> *
-- Either is a type constructor with two parameters

The kind $*$ (a.k.a. $\mathtt{Type}$) is the kind of ordinary types, the ones that have values. $\mathtt{Maybe}$ is not a type but a type constructor: a function at the type level that takes a type (say, $\mathtt{Int}$) and returns a type ($\mathtt{Maybe\;Int}$). Classes differ in the kind of their parameter: $\mathtt{Eq}$ — equality comparison — wants an ordinary type $*$, while $\mathtt{Functor}$ wants a constructor $*$ $\to *$: a container can be a functor, a value cannot. Partial application works at the type level too: $\mathtt{Either}$ has kind $*$ $\to *$ $\to *$, but $\mathtt{Either\;e} \mathbin{\mathtt{::}} *$ $\to *$ is already a legitimate functor.