Бикатегории в Haskell

Я пытаюсь определить класс типа для бикатегорий и создать его экземпляр с бикатегорией категорий, функторов и естественных преобразований.

{-# 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))

Композиция двух функторов должна быть функтором. Однако следующий экземпляр не принимается Haskell, потому что 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) }

Вот класс для бикатегорий (операторы .| и .- - это соответственно вертикальная и горизонтальная композиции для 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))

typeclass haskell category-theory
person Bob    schedule 08.08.2014    source источник
comment
f и g - это переменные уровня типа, а не переменные уровня значения.   -  person David Young    schedule 09.08.2014
comment
@DavidYoung: Я понимаю это. Но это можно сделать на бумаге. Итак, мой вопрос: как сделать то же самое в Haskell?   -  person Bob    schedule 09.08.2014
comment
Вы не указали экземпляр Category для c и e (и вы также не задали им Category ограничение), поэтому это невозможно. Как написано, fmap должен работать для всех возможных вариантов c и e. Есть неявный forall. Например, что он будет делать, если c равно Const, а e равно Tagged?   -  person David Young    schedule 09.08.2014

Ответы (1)


arrow_upward
5
arrow_downward

Давайте немного упростим составление функторов, определив получатель записи для 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.

person rampion    schedule 08.08.2014
comment
Спасибо, @rampion. Мне все еще нужно выработать ваш ответ, но, похоже, он отвечает на первую часть моего вопроса. Аналогичен ли ответ на вторую часть (т. Е. Последнюю часть моего сообщения)? - person Bob; 09.08.2014
comment
Вы почти там. Но я боюсь, что не могу принять этот ответ, поскольку он ограничен эндофункторами. - person Bob; 09.08.2014
comment
Расширение AllowAmbiguousTypes не поддерживается GHC 7.6.3, но ваш код будет принят после удаления этого расширения. Однако меня смущает используемый вами класс Arr. Похоже, что это позволяет преобразовать любую функцию Haskell типа x -> y в морфизм типа c x y категории c. Но категория не обязательно содержит все функции Haskell как морфизмы. - person Bob; 10.08.2014
comment
Боб: Верно, но вам нужен способ поднять _1 _ / _ 2_ от функций к морфизму. В качестве альтернативы вы можете потребовать, чтобы категории, которые вы хотите создать, Functor и Bicategory экземпляры для всех поддерживали class Composable c where compose :: c (g (f x)) (Compose g f x) ; uncompose :: c (Compose g f x) (g (f x)). - person rampion; 10.08.2014
comment
Боб: в качестве альтернативы вы можете определить arr как простую функцию, а не как член типа lass, с помощью arr :: (Category c, Functor (->) (->) (c x)) => (x -> y) -> c x y; arr f = fmap f id. Но опять же, это ограничило бы количество категорий, о которых вы могли бы говорить. - person rampion; 10.08.2014
comment
Боб: еще вопросы? - person rampion; 11.08.2014
comment
Больше никаких вопросов. Вот и все. Спасибо. - person Bob; 13.08.2014