# Can we define the Functor Category in Haskell (or any other language with a more expressive type system)?

Here I am talking about the Functor category, which is defined as a category whose objects are functors and morphisms are natural transformations.

For reference: https://ncatlab.org/nlab/show/functor+category

I was wondering if it is possible to define this in Haskell.

If we define category like this:

class Category cat where
id :: cat a a
(.) :: cat b c -> cat a b -> cat a c


Now how do we define Functor as an instance of this, given that Functor is itself a typeclass?

## EDIT

I am not tied to the above definition of a Category. I see Edward Kmett represents a Category like this:

newtype Yoneda (p :: i -> i -> *) (a :: i) (b :: i) = Op { getOp :: p b a }

type family Op (p :: i -> i -> *) :: i -> i -> * where
Op (Yoneda p) = p
Op p = Yoneda p

class Vacuous (a :: i)
instance Vacuous a

class Category (p :: i -> i -> *) where
type Ob p :: i -> Constraint
type Ob p = Vacuous

id :: Ob p a => p a a
(.) :: p b c -> p a b -> p a c


I am not looking for Haskell specific implementation, but in any functional language in general.

• Is your question about implementing this in Haskell? If so, it is off-topic here. Otherwise, if you're asking about how to define this concept in (functional) languages in general, this could be on-topic. In that case, it is good to clarify this. – Discrete lizard Apr 11 '18 at 8:46

Ed Kmett has actually defined this in his Hask library. The trick is to define a natural transformation as a data type and encoding the functors that this natural transformations map, in the type level like this:

class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f

data Nat (p :: i -> i -> *) (q :: j -> j -> *) (f :: i -> j) (g :: i -> j) where
Nat :: ( FunctorOf p q f
, FunctorOf p q g
) => {
runNat :: forall a. Ob p a => q (f a) (g a)
} -> Nat p q f g


Now he defines the Natural transformation as instances of a Category like this:

instance (Category' p, Category' q) => Category' (Nat p q) where
type Ob (Nat p q) = FunctorOf p q
id = Nat id1 where
id1 :: forall f x. (Functor f, Dom f ~ p, Cod f ~ q, Ob p x) => q (f x) (f x)
id1 = id \\ (ob :: Ob p x :- Ob q (f x))
observe Nat{} = Dict
Nat f . Nat g = Nat (f . g)
unop = getOp