Каковы отношения между профункторами и стрелками?

По-видимому, каждый Arrow является Strong профунктор. Действительно ^>> и >>^ соответствуют lmap и rmap. А first' и second' - это то же самое, что first и second. Аналогично каждый ArrowChoice также является Choice.

Чего не хватает профункторам по сравнению со стрелками, так это умения их составлять. Если мы добавим композицию, получим ли мы стрелу? Другими словами, если (сильный) профунктор также является категорией , то это уже стрела? Если нет, то что пропал?
2 16
haskell arrows functor

2 ответа:

Чего не хватает профункторам по сравнению со стрелками, так это умения их составлять. Если мы добавим композицию, получим ли мы стрелу?

Моноиды

Это именно тот вопрос, который рассматривается в разделе 6" понятия вычисления как моноиды, "который распаковывает результат из (довольно плотной)"категориальной семантики для стрелок ". "Понятия" - отличная статья, потому что, хотя она погружается глубоко в теорию категорий, она (1) не предполагает, что у читателя есть больше, чем поверхностное знание абстрактной алгебры и (2) иллюстрирует большую часть вызывающей мигрень математики с помощью кода Хаскелла. Мы можем кратко резюмировать раздел 6 статьи здесь:

Скажем, у нас есть 

class Profunctor p where
  dimap :: (contra' -> contra) -> (co -> co') -> p contra co -> p contra' co'

Ваша болотная стандартная, отрицательно-положительная делительная кодировка профункторов в Хаскелле. Теперь этот тип данных, 

data (⊗) f g contra co = forall x. (f contra x) ⊗ (g x co)

Как реализовано в данных.Профунктор.Композиция , действует как композиция для профунктора. Мы можем, например, продемонстрировать законный пример Profunctor: 

instance (Profunctor f, Profunctor g) => Profunctor (f ⊗ g) where
  dimap contra co (f ⊗ g) = (dimap contra id f) ⊗ (dimap id co g)
Мы будем махать рукой в доказательство того, что это законно по причинам времени и пространства.

Хорошо. А теперь самое интересное. Скажем мы этот типкласс: 

class Profunctor p => ProfunctorMonoid p where
  e :: (a -> b) -> p a b
  m :: (p ⊗ p) a b -> p a b
Это, с гораздо большим размахиванием руками, способ кодирования понятия профункторных моноидов в Хаскелле. В частности, это моноид в моноидальной категории Pro, которая является моноидальной структурой для категории функторов [C^op x C, Set] с ⊗ в качестве тензора и Hom в качестве его единицы. Так что есть много ультраспецифичных математическая дикция, чтобы распаковать здесь, но для этого вы должны просто прочитать бумагу. Тогда мы видим, что ProfunctorMonoid изоморфно Arrow... почти. 
instance ProfunctorMonoid p => Category p where
  id = dimap id id
  (.) pbc pab = m (pab ⊗ pbc)

instance ProfunctorMonoid p => Arrow p where
  arr = e
  first = undefined

instance Arrow p => Profunctor p where
  lmap = (^>>)
  rmap = (>>^)

instance Arrow p => ProfunctorMonoid p where
  e = arr
  m (pax ⊗ pxb) = pax >> pxb
Конечно, мы игнорируем здесь законы классификации типов, но, как показывает статья, они действительно работают фантастически.

Теперь я сказал почти потому, что критически мы не смогли реализовать first. То, что мы действительно сделали, продемонстрировало изоморфизм между ProfunctorMonoid и пред-стрелками .Газета называет Arrow без first a pre-arrow . Затем он продолжает показывать, что 

class Profunctor p => StrongProfunctor p where
  first :: p x y -> p (x, z) (y, z)

class StrongProfunctor p => StrongProfunctorMonoid p where
  e :: (a -> b) -> p a b
  m :: (p ⊗ p) a b -> p a b

Является необходимым и достаточным для искомого изоморфизма Arrow. Слово "сильный" происходит от конкретного понятия в теории категорий и описывается в статье лучше и богаче подробностями, чем я когда-либо мог собрать.

Итак, подведем итог:

  • Моноид в категории профункторов-это пре-стрелка, и наоборот. (В предыдущей версии статьи использовался термин " слабые стрелки" вместо предварительных стрел, и это тоже нормально, я думаю.)

  • Моноид в категории сильных профункторов-это стрела, и наоборот.

  • Поскольку монада является моноидом в категории эндофункторов, мы можем думать об аналогии SAT Functor : Profunctor :: Monad : Arrow. В этом и заключается реальная направленность статьи "понятия вычислений как моноидов".

  • Моноиды и моноидальные категории-это нежные морские существа, которые появляются повсюду, и это позор, что некоторые студенты пойдут через компьютерную науку или программное инженерное образование, не обучаясь моноидам.

  • Теория категорий-это весело.

  • Хаскелл-это весело.

25

Ответ @ haoformayor (и ссылочная статья) - это большое понимание лежащей в основе теории категорий-моноидальные категории довольно красивы! - но я подумал, что некоторый код, показывающий вам, как превратить Arrow в Strong Category и наоборот, как они появляются в соответствующих библиотеках, может быть полезным дополнением.

import Control.Arrow
import Control.Category
import Data.Profunctor
import Data.Profunctor.Strong
import Prelude hiding (id, (.))

Один путь...

newtype WrapP p a b = WrapP { unwrapP :: p a b }

instance Category p => Category (WrapP p) where
    id = WrapP id
    WrapP p . WrapP q = WrapP (p . q)

instance (Category p, Strong p) => Arrow (WrapP p) where
    first = WrapP . first' . unwrapP
    second = WrapP . second' . unwrapP

    -- NB. the first usage of id comes from (->)'s Category instance (id :: a -> a)
    -- but the second uses p's instance (id :: p a a)
    arr f = WrapP $ dimap f id id

... и еще одно...

newtype WrapA p a b = WrapA { unwrapA :: p a b }

instance Arrow p => Profunctor (WrapA p) where
    dimap f g p = WrapA $ arr f >>> unwrapA p >>> arr g

instance Arrow p => Strong (WrapA p) where
    first' = WrapA . first . unwrapA
    second' = WrapA . second . unwrapA
3