Category theory is a modern mathematical theory and a branch of abstract algebra focused on the nature of connectedness and relation. It is useful for giving solid foundations and common language to many highly reusable programming abstractions. Haskell uses Category theory as inspiration for some of the core typeclasses available in both the standard library and several popular third-party libraries.
Functor typeclass says that if a type
Functor (for which we write
Functor F) then we have a generic operation
fmap :: (a -> b) -> (F a -> F b)
which lets us "map" over
F. The standard (but imperfect) intuition is that
F a is a container full of values of type
fmap lets us apply a transformation to each of these contained elements. An example is
instance Functor Maybe where fmap f Nothing = Nothing -- if there are no values contained, do nothing fmap f (Just a) = Just (f a) -- else, apply our transformation
Given this intuition, a common question is "why not call
Functor something obvious like
The reason is that Functor fits into a set of common structures in Category theory and therefore by calling
Functor "Functor" we can see how it connects to this deeper body of knowledge.
In particular, Category Theory is highly concerned with the idea of arrows from one place to another. In Haskell, the most important set of arrows are the function arrows
a -> b. A common thing to study in Category Theory is how one set of arrows relates to another set. In particular, for any type constructor
F, the set of arrows of the shape
F a -> F b are also interesting.
So a Functor is any
F such that there is a connection between normal Haskell arrows
a -> b and the
F a -> F b. The connection is defined by
fmap and we also recognize a few laws which must hold
forall (x :: F a) . fmap id x == x forall (f :: a -> b) (g :: b -> c) . fmap g . fmap f = fmap (g . f)
All of these laws arise naturally from the Category Theoretic interpretation of
Functor and would not be as obviously necessary if we only thought of
Functor as relating to "mapping over elements".
C consists of:
Hom(C)) of morphisms between those objects. If
Obj(C), then a morphism
Hom(C)is typically denoted
f : a -> b, and the collection of all morphism between
a : Obj(C)there exists a morphism
id : a -> a;
.), taking two morphisms
f : a -> b,
g : b -> cand producing a morphism
a -> c
which obey the following laws:
For all f : a -> x, g : x -> b, then id . f = f and g . id = g
For all f : a -> b, g : b -> c and h : c -> d, then h . (g . f) = (h . g) . f
In other words, composition with the identity morphism (on either the left or right) does not change the other morphism, and composition is associative.
In Haskell, the
Category is defined as a typeclass in Control.Category:
-- | A class for categories. -- id and (.) must form a monoid. class Category cat where -- | the identity morphism id :: cat a a -- | morphism composition (.) :: cat b c -> cat a b -> cat a c
In this case,
cat :: k -> k -> * objectifies the morphism relation - there exists a morphism
cat a b if and only if
cat a b is inhabited (i.e. has a value).
c are all in
Obj(C) itself is represented by the kind
k - for example, when
k ~ *, as is typically the case, objects are types.
The canonical example of a Category in Haskell is the function category:
instance Category (->) where id = Prelude.id (.) = Prelude..
Another common example is the
Kleisli arrows for a
newtype Kleisli m a b = Kleisli (a -> m b) class Monad m => Category (Kleisli m) where id = Kleisli return Kleisli f . Kleisli g = Kleisli (f >=> g)
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.
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
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 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.
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
(-> r) are functors in Hask.
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.
In category theory, the product of two objects X, Y is another object Z with two projections: π₁ : Z → X and π₂ : Z → Y; such that any other two morphisms from another object decompose uniquely through those projections. In other words, if there exist f₁ : W → X and f₂ : W → Y, exists a unique morphism g : W → Z such that π₁ ○ g = f₁ and π₂ ○ g = f₂.
This translates into the Hask category of Haskell types as follows,
Z is product of
-- if there are two functions f1 :: W -> A f2 :: W -> B -- we can construct a unique function g :: W -> Z -- and we have two projections p1 :: Z -> A p2 :: Z -> B -- such that the other two functions decompose using g p1 . g == f1 p2 . g == f2
The product type of two types
B, which follows the law stated above, is the tuple of the two types
(A,B), and the two projections are
snd. We can check that it follows the above rule, if we have two functions
f1 :: W -> A and
f2 :: W -> B we can decompose them uniquely as follow:
decompose :: (W -> A) -> (W -> B) -> (W -> (A,B)) decompose f1 f2 = (\x -> (f1 x, f2 x))
And we can check that the decomposition is correct:
fst . (decompose f1 f2) = f1 snd . (decompose f1 f2) = f2
The choice of
(A,B) as the product of
B is not unique. Another logical and equivalent choice would have been:
data Pair a b = Pair a b
Moreover, we could have also chosen
(B,A) as the product, or even
(B,A,()), and we could find a decomposition function like the above also following the rules:
decompose2 :: (W -> A) -> (W -> B) -> (W -> (B,A,())) decompose2 f1 f2 = (\x -> (f2 x, f1 x, ()))
This is because the product is not unique but unique up to isomorphism. Every two products of
B do not have to be equal, but they should be isomorphic. As an example, the two different products we have just defined,
(B,A,()), are isomorphic:
iso1 :: (A,B) -> (B,A,()) iso1 (x,y) = (y,x,()) iso2 :: (B,A,()) -> (A,B) iso2 (y,x,()) = (x,y)
It is important to remark that also the decomposition function must be unique. There are types which follow all the rules required to be product, but the decomposition is not unique. As an example, we can try to use
(A,(B,Bool)) with projections
fst . snd as a product of
decompose3 :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool))) decompose3 f1 f2 = (\x -> (f1 x, (f2 x, True)))
We can check that it does work:
fst . (decompose3 f1 f2) = f1 x (fst . snd) . (decompose3 f1 f2) = f2 x
But the problem here is that we could have written another decomposition, namely:
decompose3' :: (W -> A) -> (W -> B) -> (W -> (A,(B,Bool))) decompose3' f1 f2 = (\x -> (f1 x, (f2 x, False)))
And, as the decomposition is not unique,
(A,(B,Bool)) is not the product of
B in Hask
The categorical product of two types A and B should contain the minimal information necessary to contain inside an instance of type A or type B. We can see now that the intuitive coproduct of two types should be
Either a b. Other candidates, such as
Either a (b,Bool), would contain a part of unnecessary information, and they wouldn't be minimal.
The formal definition is derived from the categorical definition of coproduct.
A categorical coproduct is the dual notion of a categorical product. It is obtained directly by reversing all the arrows in the definition of the product. The coproduct of two objects X,Y is another object Z with two inclusions: i_1: X → Z and i_2: Y → Z; such that any other two morphisms from X and Y to another object decompose uniquely through those inclusions. In other words, if there are two morphisms f₁ : X → W and f₂ : Y → W, exists a unique morphism g : Z → W such that g ○ i₁ = f₁ and g ○ i₂ = f₂
The translation into the Hask category is similar to the translation of the product:
-- if there are two functions f1 :: A -> W f2 :: B -> W -- and we have a coproduct with two inclusions i1 :: A -> Z i2 :: B -> Z -- we can construct a unique function g :: Z -> W -- such that the other two functions decompose using g g . i1 == f1 g . i2 == f2
The coproduct type of two types
B in Hask is
Either a b or any other type isomorphic to it:
-- Coproduct -- The two inclusions are Left and Right data Either a b = Left a | Right b -- If we have those functions, we can decompose them through the coproduct decompose :: (A -> W) -> (B -> W) -> (Either A B -> W) decompose f1 f2 (Left x) = f1 x decompose f1 f2 (Right y) = f2 y
Functor allows one to map any type
a (an object of Hask) to a type
F a and also map a function
a -> b (a morphism of Hask) to a function with type
F a -> F b. This corresponds to a Category Theory definition in a sense that functor preserves basic category structure.
A monoidal category is a category that has some additional structure:
Taking a pair as our product, this definition can be translated to Haskell in the following way:
class Functor f => Monoidal f where mcat :: f a -> f b -> f (a,b) munit :: f ()
Applicative class is equivalent to this
Monoidal one and thus can be implemented in terms of it:
instance Monoidal f => Applicative f where pure x = fmap (const x) munit f <*> fa = (\(f, a) -> f a) <$> (mcat f fa)