Representable Functors: Practical Examples

Today, we're going to be taking a look at representable functors in Haskell. But first, some incantations:

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

We recall that a natural transformation between two functors is of the type:

type Nat f g = forall x. f x -> g x

Intuitively, a natural transformation between two functors is a function between functors. for any f x, we have a recipe on how to convert it into g x. An example is the natural transformation from Maybe to List:

-- maybe2list :: Nat Maybe List
maybe2list ::  forall a. Maybe a -> List a
maybe2list Nothing = []
maybe2list (Just a) = [a]

Also recall that the function type a -> b is also called as Hom(a, b) or Hom a b. To stay consistent with category theory terminology, we're going to create a type synonym:

type Hom a b = a -> b

Now, a functor f is saif to be representable if it is the same to Hom a for some a. Let's meditate on this a little bit. So, we have:

1. A functor f
2. An object a, such that f is the same as Hom a
3. A way to convert f into Hom a. That is, we have a natural transformation from f to Hom a. This is the same as asking for Nat f (Hom a), or forall x. f x -> Hom a x, which is the same as forall x. f x -> (a -> x).
4. We also want a way to convert Hom a into f, since f is "the same" as Hom a. This asks for a Nat (Hom a) f, or a forall x. Hom a x -> f x or forall x. (a -> x) -> f x.

Intuitively, this is telling us that there's some object a such that f x is always equal to a -> x for any choice of x. So we get an equivalence beween some "data" f x, and a function a -> x. How do we encode this in haskell? What's an example? Let's see!

Haskell encoding

-- Functor f is representable iff isomorphic to SOME hom functor
-- f: C -> Set -- set to be isomorphic to hom functor
-- ∃d∈C, f ~= Hom(d, -)
-- d is called as the "representing object" of functor f
class Functor f => Representable f where
    type family RepresentingObj f :: *
    -- fwd :: Nat f (Hom d)
    -- fwd :: forall x. f x ->  (Hom d) x
    fwd :: forall x. f x ->  (RepresentingObj f -> x) 
    bwd :: forall x. (RepresentingObj f -> x) -> f x -- memoization

The idea is encoded as shown above, where we say that a functor f is Representable, if (1) it has a RepresentingObj f which represents it, and (2) there are functions to convert f x into (RepresentingObj f -> x).

Prototypical example: Streams

Consider the data type of infinite streams:

-- | always infinite stream
data Stream a = SCons a (Stream a)

for example, the infinite stream of zeros is an inhabitant of this:

zeros :: Stream Int
zeros = SCons 0 zeros

as is the stream of all natural numbers:

nats :: Stream Int
nats = let go n = SCons n (go (n+1)) in go 0

This is a functor, similar to how list is a functor:

instance Functor Stream where
    fmap f (SCons x xs) = SCons (f x) (fmap f xs)

More interestingly, it is a representable functor, since we can think of a Stream a as a function (Integer -> a), as we can index a stream at an arbitrary integer. Similarly, given an (Integer -> a), we can build a Stream a from it by memoizing the function (Integer -> a) into the data structure Stream a:

instance Representable Stream where
    type RepresentingObj Stream = Integer
    -- fwd:: Stream a -> (Integer -> a)
    fwd (SCons x _) 0 = x
    fwd (SCons _ xs) n = fwd xs (n-1)

    -- bwd:: (Integer -> a) -> Stream a
    bwd int2x = go 0 where
        go n = SCons (int2x n) (go (n+1))

Clearly, these are invertible, and thus we witness the equality between Stream a and Integer -> a

Non-example: Lists

Lists are an example of a type that is not a representable functor, because different lists can contain a different numbers of elements. so, for example, we can't use Integer as the representing object (ie, we can't write all lists as functions Natural -> a, because the empty list contains no elements, so it would have to be a function Empty -> a, while the list containing one element has a single element, so it would be the function () -> a, the list containing two elements has two elements, which would be the function Bool -> a, and so on.

Thus, it's impossible for us to find a representing object for a list!

Crazy example: Vectors

Since we saw that lists aren't representable, because we can query "outside their domain", the question naturally becomes, can we build a data structure such that the query remains within the domain? The answer is yes, with much trickery!

First, we'll need an encoding of natural numbers as 0 and a successor function (intuitively, +1), where we represent a number n as adding 1 n times to 0:

data NAT = ZERO | SUCC NAT deriving(Eq)

so, zero will be ZERO, one will be SUCC ZERO, two will be SUCC (SUCC ZERO), and so on. We implement countNAT to convert naturals to integers:

countNAT :: NAT -> Int
countNAT ZERO = 0
countNAT (SUCC n) = countNAT n + 1
instance Show NAT where show n = show (countNAT n)

Next, we create a type FinSet (n :: NAT) :: *, where FinSet n contains EXACTLY n members. Yes, that statement has a lot to unpack:

The type FinSet n has n :: NAT. So we can ask for FinSet ZERO, FinSet (SUCC ZERO), FinSet (SUCC (SUCC ZERO)) and so on. Notice that in reality, ZERO, SUCC ZERO and so on are values in Haskell. However, we are creating a type FinSet n which depends on values. To enable this, we use the DataKinds extension. Such types which can dependent on values fall under a class of type systems known as dependent types.

Let's first see the definition, and then try and gain some intuition of how this works:

data FinSet (n :: NAT) where
    Intros :: FinSet (SUCC n)
    Lift :: FinSet n -> FinSet (SUCC n)

Why does this work? I claim that FinSet n only has n numbers. Well, let's see. Can I ever crete a member of FinSet ZERO? No, both the constructors Intros and Lift create FinSet (Succ _) for some _, so it's impossible to get my hands on a FinSet ZERO. What about FinSet (SUCC ZERO) [aka FinSet 1]? Yes, there's one way to get such an element:

Intros :: FinSet (SUCC ZERO)

and that's the only way to get a member of FinSet (SUCC ZERO)! What about FinSet (SUCC (SUCC ZERO))? We have two inhabitants:

FinSet (SUCC (SUCC ZERO))
- Intros :: FinSet (SUCC (SUCC ZERO))
- Lift (Intros :: FinSet (SUCC ZERO)) :: FinSet (SUCC (SUCC ZERO))

and so on. Here's the Show instance for a FinSet, where we think of Intros as 1, and Lift as incrementing the number.

countFinSet :: FinSet n -> Int
countFinSet Intros = 1
countFinSet (Lift x) = 1 + countFinSet x

instance Show (FinSet n) where
    show x = show (countFinSet x)

We can use the same mechanism to encode Vector n a, a vector with exactly n elements!

data Vector (n :: NAT) (a :: *)  where
    VNil :: Vector ZERO a
    VCons :: a -> Vector n a -> Vector (SUCC n) a

instance Functor (Vector n) where
    fmap _ VNil = VNil
    fmap f (VCons a as) = VCons (f a) (fmap f as)

instance Representable (Vector n) where
    type RepresentingObj (Vector n) = FinSet n

    -- fwd :: forall x. f x ->  (RepresentingObj f -> x) 
    fwd :: forall x. Vector n x -> ((FinSet n) -> x)
    fwd (VCons x xs) Intros = x
    fwd (VCons x xs) (Lift n) = fwd xs n

    bwd :: forall x. ((FinSet n) -> x) -> Vector n x
    bwd finset2x = undefined

Unfortunately, I couldn't quite figure out how to write bwd in Haskell, thus I leave it as an exercise for the reader :)