Подтвердить что ты не робот

Какая связь между профукаторами и стрелами?

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

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

4b9b3361

Ответ 1

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

Моноиды

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

Скажем, что

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

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

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

реализованный в Data.Profunctor.Composition, действует как композиция для профунтера. Например, мы можем продемонстрировать законный экземпляр Profunctor:

instance (Profunctor f, Profunctor g) => Profunctor (f ⊗ g) where
  dimap contra co (f ⊗ g) = (dimap contra id f) ⊗ (dimap id co g)

Мы проверим доказательство того, что оно является законным по причинам времени и пространства.

OK. Теперь самое интересное. Скажем, мы это typeclass:

class Profunctor p => ProfunctorMonoid p where
  e :: (a -> b) -> p a b
  m :: (p ⊗ p) a b -> p a b

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

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. Это реальная тяга к статье "вычисления-вычисления-моноиды".

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

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

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

Ответ 2

Ответ @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 (->) Category instance (id :: a -> a)
    -- but the second uses p 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