Haskell中的Bicategories

Question

我正在尝试为bicategories定义一个类型类,并使用类别,仿函数和自然转换的双类别来实例化它.

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

这是类别的类:

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

这是仿函数的类:

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

这是仿函数的组成:

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

两个仿函数的组合应该是一个仿函数.但是,下面的实例不会被哈斯克尔接受,因为f和g不在范围之内.你会如何定义fmap？

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

这是自然转换(这里不使用参数c,但对下面的下一个实例有用.):

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

这是bicategories的类(运算符.|,.-分别是2个单元格的垂直和水平组合):

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

类别,仿函数和自然变换应该形成一个双重类别.但是,Haskell不接受以下实例化,因为在.-自然变换的水平组成的定义中,g不在范围内.你如何在这里定义水平构图(.-)？

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

让我们通过定义记录getter Compose(无需缩写,我们是朋友之间)来组合仿函数更容易一些:

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)

为了制作Compose g f一个Functor c d,我们需要一种方法将函数提升到类别中d,所以让我们定义一个:

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

现在我们已经拥有了我们需要的一切:

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

在这里我们必须使用AllowAmbiguousTypes(在GHC 7.8中),因为该类别d完全消失,所以它是模棱两可的.

现在为Bicategory.

让我们简化一下NT- 我们不需要那个幻影参数.

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

现在我们可以做一个更简单的Bicategory定义:

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')

我们可以实施:

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

这是完整代码的要点.用GHC-7.8.2编译好.