Meta info

  Filled under: haskell, category theory

  Last updated: February 15, 2014

Representable functors

A functor1 \(F : C \to Set\) is called representable if it is isomorphic to \(Hom(A, -)\) for some \(A\) (denoted as \(F \simeq Hom(A,-)\)). Since we are talking about Haskell, I’ll also use the \((a \to -)\) notation instead of \(Hom(a, -)\).

The object \(A\) is called representing object for a functor \(F\). Usually, the isomorphism between the functor is given by two natural transformations.

Throughout the text the letters \(\alpha\) and \(\beta\) are used to denoted those natural transformations. That is, \(\alpha : (a \to -) \Rightarrow F\), \(\beta : F \Rightarrow (a \to -)\) and \(\alpha \circ \beta = \beta \circ \alpha = \mathord{id}\)

You can find the Haskell version of the definitions and operations in this document in the Data.Functor.Rep module (written by Edward Kmett). Using Haskell notation we say that representable Functor f is isomorphic to ((->) e for a representing object e.

Examples

Reader

The reader functor Reader r

newtype Reader r a = Reader { 
    runReader :: r -> a
    }

instance Functor (Reader r) where
    fmap f m = Reader $ \r ->
        f (runReader m r)

is trivially isomorphic to ((->) r for every r.

Identity

The identity functor is defined as

newtype Identity a = Identity { runIdentity :: a }
instance Functor Identity where
    fmap f (Identity a) = Identity $ f a

Identity is represented by the unit type ().

alpha f = Identity (f ())
beta (Identity k) = \() -> k

alpha . beta == beta . alpha == id

beta (alpha f)
= beta (Identity (f ()) 
= \() -> f ()
= f

alpha (beta k) 
= alpha (\() -> runIdentity k)
= Identity ((\() -> runIdentity k) ())
= Identity (runIdentity k)
= k

Homogeneous pairs

data Pair a = P a a
instance Functor Pair where
    fmap f (P a a) = P (f a) (f a)

This Pair functor is representable by the type Bool.

alpha :: (Bool -> a) -> Pair a
alpha f = P (f True) (f False)
beta :: Pair a -> (Bool -> a)
beta (P x y) = \b -> case b of
    True  -> x
    False -> y

In fact, we can go even further: the functor data Triple a = T a a a is representable by the type data Three = One | Two | Three and so on. This method can be generalized to vectors of fixed length.

Streams

Streams are basically infinite lists and they can be represented by natural numbers.

Pascal Hof has elaborated on this matter in his blog post.

Representable implies monad

Every representable functor in Haskell is in fact a monad, what is more – a monad isomorphic to Reader. Assume that the \(F \simeq (a \to -)\) isomorphism is defined by the natural transformations \(\alpha : (a \to -) \Rightarrow F\), \(\beta : F \Rightarrow (a \to -)\). Then the monadic operations is defined as following:

return :: x -> f x
return x = alpha $ \_ -> x = alpha (const x)

(>=>) :: (x -> f y) -> (y -> f z) -> (x -> f z)
(f >=> g) x = alpha $ \a -> beta (g (beta (f x) a)) a

join :: f (f x) -> f x
join v = alpha $ \a -> beta (beta v a) a

We can prove that f indeed is a Monad. You can find a formalized Coq proof of this fact here. Equational reasoning can be used to prove the usual monad laws:

-- return >=> g = g
(return >=> g) x
= alpha $ \a -> beta (g (beta (return x) a)) a
= alpha $ \a -> beta (g (beta (alpha (const x)) a)) a
-- alpha and beta are ISO
= alpha $ \a -> beta (g ((const x) a)) a
= alpha $ \a -> beta (g x) a
-- alpha and beta are iso
= g x
-- g >=> return = g
(g >=> return) x
= alpha $ \a -> beta (return (beta (g x) a)) a
= alpha $ \a -> beta (alpha (const (beta (g x) a))) a
-- alpha and beta are iso
= alpha $ \a -> (const (beta (g x) a)) a
= alpha $ \a -> beta (g x) a
-- alpha and beta are iso
= g x
-- (f >=> g) >=> h = f >=> (g >=> h)
((f >=> g) >=> h) x 
= alpha $ \a -> beta (h (beta ((f >=> g) x) a)) a
= alpha $ \a -> beta (h (beta (alpha $ \a -> beta (g (beta (f x) a)) a) a)) a
-- alpha and beta are iso
= alpha $ \a -> beta (h ((\a -> beta (g (beta (f x) a)) a) a)) a
= alpha $ \a -> beta (h (beta (g (beta (f x) a)) a)) a

(f >=> (g >=> h)) x 
= alpha $ \a -> beta ((g >=> h) (beta (f x) a)) a
-- unfolding the definition
= alpha $ \a -> beta (alpha $ \a -> beta (h (beta (g (beta (f x) a)) a)) a) a
-- alpha and beta are iso
= alpha $ \a -> (\a -> beta (h (beta (g (beta (f x) a)) a)) a) a
= alpha $ \a -> beta (h (beta (g (beta (f x) a)) a)) a

Operations

“Representability” of functors is preserved by the product, composition operations

NB: Additional explanation is necessary

Non-representable functors

Some functors can not be represented by any objects; such functors are called, as you have probably guessed, non-representable. The examples of such functors are provided below; it is also shown how to prove that a specific functor is non-representable.

Examples

Maybe

Maybe is a simple non-representable functor. This fact can be proved by contradiction.

Assume there is a such that \(\mathord{Maybe} \simeq (a \to -)\); the equivalence is defined by the natural transformations \(\eta : (a \to -) \Rightarrow \mathord{Maybe}\), \(\eta^{-1} : \mathord{Maybe} \Rightarrow (a \to -)\). In particular,

\[\mathord{Maybe}\;a \simeq a \to a\]

That means that there exists some \(u : \mathord{Maybe}\:a\) that corresponds to \(id_a\). \[u = \eta_a(id_a)\]

Due to the naturality of \(\eta\), the following holds for every type \(b\) and for every function \(g : a \to b\)

\[\mathord{fmap}\; g\; \eta_a(id) = \mathord{fmap}\; g\; u = \eta_b(g\circ id) = \eta_b(g)\]

Commutative diagram for a natural transformation
Commutative diagram for a natural transformation

Case 1: \(u = \mathord{Just} \; \mathord{x}\) for some \(x : a\).

In this case, \(\mathord{fmap}\; g\; u = \mathord{Just}\; (g\;x) = \eta_b(g)\). Since this holds for all \(b\) and \(g\), \(\mathord{Nothing} : \mathord{Maybe}\; b\) does not correspond to any function \((a \to b)\). Contradiction.

Case 2: \(u = \mathord{Nothing}\).

In this case, \(\mathord{fmap}\; g\; u = \mathord{Nothing} = \eta_b(g)\). Since this holds for all \(b\) and \(g\), \(\mathord{Just}\;x : \mathord{Maybe}\; b\) (for some \(x : b\)) does not correspond to any function \((a \to b)\). Contradiction.

Either

Since Maybe a is isomorphic to Either () a and to Either a (), we can conclude that the Either x functor is not representable in general.

Lists

Only vectors (of definite and un-varying length) and streams (lists of infinite length) are representable.

Acknowledgments

I would like to thank Cale Gibbard for reviewing some of the proofs and Edward Kmett for explaining some of the stuff from his libraries to me.

Discussion

Edward told me that if he were to write the Representable class today he would bundle tabulate and index in one isomorphism.

Please feel free to provide commentary and additional information using the form below; alternatively you can reach me by email dan [at] this-server


  1. If you want to sound cool, you can also use the term presheaf, although the story is a little bit different in this case

 Comment section!
comments powered by Disqus