Bicategories in Haskell

Question

I am trying to define a type class for bicategories and instantiate it with the bicategory of categories, functors and natural transformations.

{-# LANGUAGE NoImplicitPrelude, MultiParamTypeClasses, 
    TypeOperators, KindSignatures, Rank2Types, 
    ScopedTypeVariables, FlexibleInstances, InstanceSigs #-}

Here is the class for categories:

class Category (c :: * -> * -> *) where
  id :: c x x
  (.) ::c y z -> c x y -> c x z

Here is the class for functors:

class Functor c d f where
  fmap :: c x y -> d (f x) (f y)

Here is the composition of functors:

newtype Comp g f t = Comp (g (f t))

The composition of two functors should be a functor. However, the following instantiation is not accepted by Haskell because f and g are not in scope. How would you define fmap here?

instance Functor c e (Comp g f) where
  fmap :: c x y -> e (Comp g f x) (Comp g f y) 
  fmap = fmap g . fmap f

Here are natural transformations (The parameter c is not used here but is useful for the next instantiation below.):

newtype NT f g (c :: * -> * -> *) d =
  NT {unNT :: forall x. d (f x) (g x) }

Here is the class for bicategories (The operators .| and .- are respectively the vertical and horizontal compositions for 2-cells):

class Bicategory
  (bicat :: (* -> *) -> (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *)
  comp where
  id1 :: Category d => bicat f f c d
  (.|) :: Category d => bicat g h c d -> bicat f g c d -> bicat f h c d
  (.-) :: bicat g g' d e -> bicat f f' c d -> bicat (g `comp` f) (g' `comp` f') c e

Categories, functors and natural transformations should form a bicategory. However, the following instantiation is not accepted by Haskell because, in the definition of the horizontal composition .- of natural transformations, g in not in scope. How would you define the horizontal composition (.-) here?

instance Bicategory NT Comp where
  id1 = NT id
  n .| m = NT (unNT n . unNT m)
  (n :: NT g g' d e) .- m = NT (unNT n . fmap g (unNT m))

Answer 1

Let's make it a little easier to compose functors by defining a record getter for Compose (no need to abbreviate, we're among friends):

newtype Compose g f t = Compose { unCompose :: g (f t) }
-- Compose    :: g (f t) -> Compose g f t
-- unCompose  :: Compose g f t -> g (f t)

In order to make Compose g f a Functor c d, we need a way to lift functions into the category d, so let's define one:

class Category c => Arr c where
  arr :: (x -> y) -> c x y -- stolen from Control.Arrow.Arrow

Now we've got everything we need:

instance (Functor c d f, Functor d e g, Arr e) => Functor c e (Compose g f) where
  -- c                      :: c x y
  -- fmap_cdf c             :: d (f x) (f y)
  -- fmap_deg (fmap_cdf c)  :: e (g (f x)) (g (f y))
  -- arr Compose            :: e (g (f y)) (Compose g f y)
  -- arr unCompose          :: e (Compose g f x) (g (f x))
  -- arr Compose . fmap_deg (fmap_cdf c) . arr unCompose 
  --                        :: e (Compose g f x) (Compose g f y)
  fmap c = arr Compose . fmap_deg (fmap_cdf c) . arr unCompose
    where fmap_cdf :: forall x y. c x y -> d (f x) (f y)
          fmap_cdf = fmap
          fmap_deg :: forall x y. d x y -> e (g x) (g y)
          fmap_deg = fmap

Here we have to use AllowAmbiguousTypes (in GHC 7.8), as the category d disappears completely, so it's ambiguous.

Now for Bicategory.

Let's simplify NT - we don't need that phantom parameter.

newtype NT c f g = NT { unNT :: forall x. c (f x) (g x) }

Now we can make a simpler Bicategory definition:

class Bicategory (bicat :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) comp where
  id1   :: Category c => bicat c f f
  (.|)  :: Category c => bicat c g h -> bicat c f g -> bicat c f h
  (.-)  :: (Functor c d g, Arr d) => bicat d g g' -> bicat c f f' -> bicat d (comp g f) (comp g' f')

Which we can implement:

instance Bicategory NT Compose where
  id1 = NT id
  NT n .| NT m = NT (n . m)
  -- m              :: c (f x) (f' x)
  -- fmap m         :: d (g (f x)) (g (f' x))
  -- n              :: d (g (f' x)) (g' (f' x))
  -- n . fmap m     :: d (g (f x)) (g' (f' x))
  -- arr Compose    :: d (g' (f' x)) (Compose g' f' x)
  -- arr unCompose  :: d (Compose g f x) (g (f x))
  -- arr Compose . n . fmap m . arr unCompose
  --                :: d (Compose g f x) (Compose g' f' x)
  NT n .- NT m = NT $ arr Compose . n . fmap m . arr unCompose

Here's a gist of the complete code. Compiles fine with GHC-7.8.2.