0
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Discrete lizard Apr 11 '18 at 8:46
0
$\begingroup$

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

All of this can be found here: https://github.com/ekmett/hask/blob/master/src/Hask/Category.hs

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.