Haskell Language Category Theory Haskell types as a category
Example
Definition of the category
The Haskell types along with functions between types form (almost†) a category. We have an identity morphism (function) (id :: a -> a) for every object (type) a; and composition of morphisms ((.) :: (b -> c) -> (a -> b) -> a -> c), which obey category laws:
f . id = f = id . f
h . (g . f) = (h . g) . f
We usually call this category Hask.
Isomorphisms
In category theory, we have an isomorphism when we have a morphism which has an inverse, in other words, there is a morphism which can be composed with it in order to create the identity. In Hask this amounts to have a pair of morphisms f,g such that:
f . g == id == g . f
If we find a pair of such morphisms between two types, we call them isomorphic to one another.
An example of two isomorphic types would be ((),a) and a for some a. We can construct the two morphisms:
f :: ((),a) -> a
f ((),x) = x
g :: a -> ((),a)
g x = ((),x)
And we can check that f . g == id == g . f.
Functors
A functor, in category theory, goes from a category to another, mapping objects and morphisms. We are working only on one category, the category Hask of Haskell types, so we are going to see only functors from Hask to Hask, those functors, whose origin and destination category are the same, are called endofunctors. Our endofunctors will be the polymorphic types taking a type and returning another:
F :: * -> *
To obey the categorical functor laws (preserve identities and composition) is equivalent to obey the Haskell functor laws:
fmap (f . g) = (fmap f) . (fmap g)
fmap id = id
So, we have, for example, that [], Maybe or (-> r) are functors in Hask.
Monads
A monad in category theory is a monoid on the category of endofunctors. This category has endofunctors as objects F :: * -> * and natural transformations (transformations between them forall a . F a -> G a) as morphisms.
A monoid object can be defined on a monoidal category, and is a type having two morphisms:
zero :: () -> M
mappend :: (M,M) -> M
We can translate this roughly to the category of Hask endofunctors as:
return :: a -> m a
join :: m (m a) -> m a
And, to obey the monad laws is equivalent to obey the categorical monoid object laws.
†In fact, the class of all types along with the class of functions between types do not strictly form a category in Haskell, due to the existance of undefined. Typically this is remedied by simply defining the objects of the Hask category as types without bottom values, which excludes non-terminating functions and infinite values (codata). For a detailed discussion of this topic, see here.
