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

40

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

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

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

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

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

Петр Пудлак
источник

Ответы:

35

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

  • Сильный endofunctor над моноидальными категориями является тот , который приходит с естественным преобразованием , удовлетворяющий некоторые условия согласованности по отношению к ассоциатору, которые я замаскирую. Это условие иногда также произносится как « имеет силу».( C , , I ) σ : A F ( B ) F ( A B ) FF:СС(С,,я)σ:AF(В)F(AВ)F

  • Слабый моноидальный функтор есть функтор между двумя моноидальными категориями и , с естественными преобразованиями и , снова удовлетворяющие условию когерентности относительно ассоциаторов.( C , , I ) ( D , , J ) ϕ : F ( A ) F ( B ) F ( A B ) i : J F ( I )F:СD(С,,я)(D,,J)φ:F(A)F(В)F(AВ)я:JF(я)

  • Сильный моноидальный функтор тот , в котором и являюсь естественными изоморфизмами. То есть , причем и его обратное описание изоморфизма.F:СDφяF(AВ)F(A)F(В)φ

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

Кроме того, в декартовой замкнутой категории имеющий силу, эквивалентен существованию естественного преобразования . То есть наличие силы означает, что функторное действие определяется как функция более высокого порядка в языке программирования.Fмaп:(AВ)(F(A)F(В))

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

Нил Кришнасвами
источник
1
Спасибо за ответ. Правильно ли я понимаю, что все экземпляры Functorимеют силу (продукт WRT) просто потому, что они определены с использованием fmapязыка? Кроме того, что меня озадачивает, что ваше определение и i перевернуто по сравнению с вашим постом в блоге и статьей в Википедии - это опечатка? Я попытался определить, используя как , что явно необходимо . φяpureipure' = \v -> fmap (\() -> v) (i ())i :: (Applicative f) => () -> f ()
Петр Пудлак
1
У меня была опечатка в этом ответе - теперь исправлено. И да, все случаи Functorсильны (по продукту).
Нил Кришнасвами
Не могли бы вы также уточнить, где стоит Монада? Если я правильно понимаю, это тоже моноидальный эндофунктор.
egdmitry
@egdmitry Моноидальный , а не монадальный . Это означает, что мы имеем дело с эндофунктором моноидальной категории (в данном случае является моноидальным по отношению к декартовому произведению, т.е. парам). Hask
Кирелагин
Могу ли я предложить использовать слово strongy, чтобы избежать столкновения обозначений с «сильным»? Это шотландская (особенно здесь точная) диалектическая вариация «сильного», впервые использованная в Библии Уиклифа.
Фоско
3

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

Из леммы Йонеды следует, что между и n a t существует изоморфизм ( H o m ( A , B ) , F B ) . В категории типов Haskell, это отображение ( г Р ( г ) ( ) ) типа F A B AF B . Оценка в F AFANaT(ЧАСом(A,В),FВ)

a(гF(г)(a))
FAВAFВ,
FAзатем, применяя карту стрелок функторов к результирующей функции - если компоненты естественного преобразования имеют смысл как стрелки - и снова абстрагируя , мы получаем отображение типа F A FFA Теперь, если функтор поставляется с монадическим «соединением», отображением из F F B в F B , и если мы переключаемся вокруг лямбда-абстракций и, следовательно, первых двух слотов аргументов, мы можем получить функцию типа F
FAFВAFFВ,
FFВFВ который обозначается через <*>. (Это также то, что вы получаете через L i f t M 2 i d в Haskell.)
FВAFAFВ,
LяеTM2 яd
Nikolaj-K
источник