Haskell binoculars

Question

I am trying to define a type class for bi-categories and create it using two categories of categories, functors and natural transformations.

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

Here is a class class for categories:

 class Category (c :: * -> * -> *) where id :: cxx (.) ::cyz -> cxy -> cxz 

Here is a class for functors:

 class Functor cdf where fmap :: cxy -> d (fx) (fy) 

Here is the composition of the functors:

 newtype Comp gft = Comp (g (ft)) 

The composition of two functors must be a functor. However, Haskell does not accept the next instance, because f and g not included in the volume. How would you define fmap here?

 instance Functor ce (Comp gf) where fmap :: cxy -> e (Comp gfx) (Comp gfy) fmap = fmap g . fmap f 

Here are the natural conversions (the c parameter is not used here, but is useful for the following instance below):

 newtype NT fg (c :: * -> * -> *) d = NT {unNT :: forall x. d (fx) (gx) } 

Here is the class for bi-categories (Operators .| And .- are respectively vertical and horizontal compositions for 2 cells):

 class Bicategory (bicat :: (* -> *) -> (* -> *) -> (* -> * -> *) -> (* -> * -> *) -> *) comp where id1 :: Category d => bicat ffcd (.|) :: Category d => bicat ghcd -> bicat fgcd -> bicat fhcd (.-) :: bicat gg' de -> bicat ff' cd -> bicat (g `comp` f) (g' `comp` f') ce 

Categories, functors, and natural transformations should form a bi-category. However, Haskell does not accept the following instance, because in the definition of horizontal composition .- natural transformations of g are not in volume. How can you define horizontal composition (.-) here?

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

Answer 1

Let me simplify the layout of functors a bit by specifying getter for Compose (no need to shorten, we are among friends):

 newtype Compose gft = Compose { unCompose :: g (ft) } -- Compose :: g (ft) -> Compose gft -- unCompose :: Compose gft -> g (ft) 

To make Compose gf a Functor cd , we need a way to raise functions to category d , so let's define one:

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

Now we have everything we need:

 instance (Functor cdf, Functor deg, Arr e) => Functor ce (Compose gf) where -- c :: cxy -- fmap_cdf c :: d (fx) (fy) -- fmap_deg (fmap_cdf c) :: e (g (fx)) (g (fy)) -- arr Compose :: e (g (fy)) (Compose gfy) -- arr unCompose :: e (Compose gfx) (g (fx)) -- arr Compose . fmap_deg (fmap_cdf c) . arr unCompose -- :: e (Compose gfx) (Compose gfy) fmap c = arr Compose . fmap_deg (fmap_cdf c) . arr unCompose where fmap_cdf :: forall x y. cxy -> d (fx) (fy) fmap_cdf = fmap fmap_deg :: forall x y. dxy -> e (gx) (gy) fmap_deg = fmap 

Here we should use AllowAmbiguousTypes (in GHC 7.8), since the category d completely disappears, so it is ambiguous.

Now for the Bicategory .

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

 newtype NT cfg = NT { unNT :: forall x. c (fx) (gx) } 

Now we can make a simpler Bicategory definition:

 class Bicategory (bicat :: (* -> * -> *) -> (* -> *) -> (* -> *) -> *) comp where id1 :: Category c => bicat cff (.|) :: Category c => bicat cgh -> bicat cfg -> bicat cfh (.-) :: (Functor cdg, Arr d) => bicat dgg' -> bicat cff' -> bicat d (comp gf) (comp g' f') 

What we can implement:

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

Here is the gist of the complete code . Compilation is excellent with GHC-7.8.2.