Siddharth Bhat
27 May 2021
•
5 min read
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:
f
a
, such that f
is the same as Hom a
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)
.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!
-- 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)
.
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
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!
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 :)
Ground Floor, Verse Building, 18 Brunswick Place, London, N1 6DZ
108 E 16th Street, New York, NY 10003
Join over 111,000 others and get access to exclusive content, job opportunities and more!