Почему Стати c Стрелки обобщают Стрелки? - PullRequest
5 голосов
/ 11 июля 2020

Широко известно, что Applicative обобщает Arrows. В идиомы не обращают внимания, стрелки точны, монады беспорядочны. имеет место следующий изоморфизм:

arr a b :<->: arr () (a -> b)

Насколько я понимаю, это можно проиллюстрировать следующим образом:

Примечание: newtype Identity a = Id { runId :: a }.

Klesli Identity - это Стати c Стрелка, охватывающая k :: a -> Identity b. Изоморфизм просто удаляет или добавляет оболочку.

Kleilsi Maybe не является Stati c Стрелка, так как k = Kleisli (const Nothing) существует - все f :: a -> b соответствуют Just . f, а * 1026 нет места * в изоморфизме.

Но в то же время и Kleisli Identity, и Kleisli Maybe являются Arrow экземплярами. Поэтому я не вижу, как работает обобщение.

В Учебник Haskell / Understanding Arrows на Wikibooks они говорят stati c морфизм и обратите внимание на следующее :

Эти две концепции обычно известны как стрелки c и стрелки Клейсли соответственно. Поскольку использование слова «стрела» с двумя слегка разными значениями сделало бы этот текст ужасно запутанным, мы выбрали «морфизм», который является синонимом этого альтернативного значения.

есть до сих пор - я путаю Haskell Arrow и стрелки?

Итак, как эта иерархия работает? Каким образом оформляется / подтверждается собственность Applicative?

1 Ответ

3 голосов
/ 11 июля 2020

Я считаю, что слово «обобщения» сбивает вас с пути. Если arr - это Arrow, действительно так:

  • arr x для любого x будет Applicative;
  • В частности, arr () будет аппликативом;
  • Затем этот аппликативный падеж может быть воспроизведен как эквивалентная c стрелка (в терминах Static из полугруппоидов , Static (arr ()) a b ~ arr () (a -> b))

Этот процесс, однако, не без потерь в общем случае: stati c стрелка Static (arr ()) не обязательно эквивалентна arr стрелке, с которой мы начали; изоморфизма быть не должно. Другими словами, stati c стрелки не обобщают стрелки. Если бы мы определили класс StaticArrow, он был бы подклассом Arrow, а не суперклассом.

PS: В цитате из Викибука формулировка здесь просто акцент. Например, хотя стрелки Клейсли действительно являются стрелками Хьюза / Control.Arrow, большую часть времени, когда люди говорят о «стрелах Клейсли», они думают не о примере Arrow, а просто о том, как они являются морфизмами в категории, в которой категория l aws составляет монаду l aws для некоторой монады. В частности, этого достаточно, чтобы сформулировать обсуждение в этом отрывке из Викибука.

...