A functor^{1} \(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`

.

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`

.

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
```

```
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 are basically infinite lists and they can be represented by natural numbers.

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

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
```

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

NB: Additional explanation is necessary

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.

`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)\]

**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.

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.

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

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.

- http://ncatlab.org/nlab/show/representable+functor
- http://hackage.haskell.org/package/adjunctions
- Representing Applicatives by Gershom Bazerman
- http://repos.covariant.me/browse?r=coq;a=headblob;f=/Rep.v

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`

Comment section!

comments powered by Disqus