Объяснение аппликативного функтора в категориальных терминах - моноидальные функторы

Я хотел бы понять Applicativeс точки зрения теории категорий.

Документация для Applicativeговорит , что это сильный слабый моноидальный функтор .

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

Во-вторых, каковы моноидальные категории Applicativeмоноидальных функторов? Я предполагаю, что функторы являются эндофункторами в стандартной категории Haskell (объекты = типы, морфизмы = функции), но я понятия не имею, что такое моноидальная структура в этой категории.

Спасибо за помощь.

lo.logic type-theory functional-programming ct.category-theory Петр Пудлак
источник

Ответы:

На самом деле здесь есть два использования слова «сила».

Сильный endofunctor над моноидальными категориями является тот , который приходит с естественным преобразованием , удовлетворяющий некоторые условия согласованности по отношению к ассоциатору, которые я замаскирую. Это условие иногда также произносится как « имеет силу». $F : C \to C$ $(C, \otimes, I)$ $\sigma : A \otimes F(B) \to F(A \otimes B)$ $F$
Слабый моноидальный функтор есть функтор между двумя моноидальными категориями и , с естественными преобразованиями и , снова удовлетворяющие условию когерентности относительно ассоциаторов. $F : C \to D$ $(C, \otimes, I)$ $(D, \oplus, J)$ $\phi : F(A) \oplus F(B) \to F(A \otimes B)$ $i : J \to F(I)$
Сильный моноидальный функтор тот , в котором и являюсь естественными изоморфизмами. То есть , причем и его обратное описание изоморфизма. $F : C \to D$ $\phi$ $i$ $F(A \otimes B) \simeq F(A) \oplus F(B)$ $\phi$

Аппликативный функтор, в смысле программ на Haskell, представляет собой слабый моноидальный эндофунктор с прочностью , причем рассматриваемая моноидальная структура является декартовым произведением. Вот почему вы получаете парадоксально звучащий термин «сильный слабый моноидальный функтор».

Кроме того, в декартовой замкнутой категории имеющий силу, эквивалентен существованию естественного преобразования . То есть наличие силы означает, что функторное действие определяется как функция более высокого порядка в языке программирования. $F$ $\mathrm{map} : (A \Rightarrow B) \to (F(A) \Rightarrow F(B))$

Наконец, если вам интересна теория типов аппликативных функторов в стиле Хаскеля, я только что написал об этом в блоге.

Нил Кришнасвами
источник

Спасибо за ответ. Правильно ли я понимаю, что все экземпляры Functorимеют силу (продукт WRT) просто потому, что они определены с использованием fmapязыка? Кроме того, что меня озадачивает, что ваше определение

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

ϕ

$\phi$

i

$i$ pureipure' = \v -> fmap (\() -> v) (i ())i :: (Applicative f) => () -> f ()

Петр Пудлак

У меня была опечатка в этом ответе - теперь исправлено. И да, все случаи Functorсильны (по продукту).

Нил Кришнасвами

Не могли бы вы также уточнить, где стоит Монада? Если я правильно понимаю, это тоже моноидальный эндофунктор.

egdmitry

@egdmitry Моноидальный , а не монадальный . Это означает, что мы имеем дело с эндофунктором моноидальной категории (в данном случае

является моноидальным по отношению к декартовому произведению, т.е. парам).

Hask

$\operatorname{Hask}$

Кирелагин

Могу ли я предложить использовать слово strongy, чтобы избежать столкновения обозначений с «сильным»? Это шотландская (особенно здесь точная) диалектическая вариация «сильного», впервые использованная в Библии Уиклифа.

Фоско

Чтобы понять Applicative, вызванный монадой, я хочу указать на следующую конструкцию:

Из леммы Йонеды следует, что между и существует изоморфизм . В категории типов Haskell, это отображение типа Оценка в $FA$ $\mathrm{nat}(\mathrm{Hom}(A,B),FB)$

a \mapsto (г \mapsto F (г) (a))

$a\mapsto\left(g\mapsto F(g)(a)\right)$

F A \to В^{A} \to F В,

$FA\to B^A\to FB.$

F A

$FA$ затем, применяя карту стрелок функторов к результирующей функции - если компоненты естественного преобразования имеют смысл как стрелки - и снова абстрагируя

, мы получаем отображение типа

F A

$FA$

Теперь, если функтор поставляется с монадическим «соединением», отображением из

, и если мы переключаемся вокруг лямбда-абстракций и, следовательно, первых двух слотов аргументов, мы можем получить функцию типа

F A \to F В^{A} \to F F В,

$FA\to F\,B^A\to FFB.$

F F B

$FFB$

F B

$FB$

который обозначается через <*>. (Это также то, что вы получаете через

в Haskell.)

F В^{A} \to F A \to F В,

$F\,B^A\to FA\to FB,$

L i f t M 2 i d

$\mathrm{LiftM2\ id}$

Nikolaj-K
источник