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

Question

Видимо, каждый Arrow это Strong profunctor. В самом деле ^>> а также >>^ соответствовать lmap а также rmap, А также first' а также second' так же, как first а также second, Точно так же каждый ArrowChoice это также Choice,

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

Answer 1

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

моноиды

Именно этот вопрос решается в разделе 6 " Понятия вычислений как моноидов", в котором распаковывается результат из (довольно плотной) " Категориальной семантики для стрелок". "Понятия" - отличная статья, потому что, хотя она глубоко погружается в теорию категорий, она (1) не предполагает, что читатель имеет более чем поверхностное знание абстрактной алгебры, и (2) иллюстрирует большую часть математики, вызывающей мигрень, с помощью кода на Haskell. Мы можем кратко изложить раздел 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)

как реализовано в Data.Profunctor.Composition, действует как композиция для profunctor. Мы можем, например, продемонстрировать законную инстанцию 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

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

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

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

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

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