Как подъем (в контексте функционального программирования) соотносится с теорией категорий?

Лифты и двойственное понятие расширений абсолютно используются в Haskell, возможно, наиболее заметно в облике комонадического extend и монадического bind. (Как ни странно, extend - это подъемник, а не расширение.) Комонада w extend позволяет нам взять функцию w a -> b и поднять ее вдоль extract :: w b -> b, чтобы получить карту w a -> w b. В ASCII art, учитывая схему

        w b
         |
         V
w a ---> b

где вертикальная стрелка извлекает, extend дает нам диагональную стрелку (заставляя диаграмму коммутировать):

     -> w b
    /    |
   /     V
w a ---> b

Большинству хаскеллеров более знакомо двойное понятие bind (>>=) для монады m. Имея функции a -> m b и return :: a -> m a, мы можем «расширить» нашу функцию вдоль return, чтобы получить функцию m a -> m b. В искусстве ASCII:

a ---> m b
|
V
m a

дает нам

a ---> m b
 |  __A
 V /
m a

(Этот A - наконечник стрелы!)

Так что да, extend можно было назвать lift, а bind можно было назвать extend. Что касается lifts Haskell, я понятия не имею, почему они так называются!

РЕДАКТИРОВАТЬ: На самом деле, я снова думаю, что lift в Haskell на самом деле являются расширениями. Если f является аппликативным и у нас есть функция a -> b -> c, мы можем составить эту функцию с pure :: c -> f c, чтобы получить функцию a -> b -> f c. Несомненно, это то же самое, что и функция (a, b) -> f c. Теперь мы также можем нажать (a, b) с помощью pure, чтобы получить функцию (a, b) -> f (a, b). Теперь, fmaping fst и snd, мы получаем функции f (a, b) -> f a и f (a, b) -> f b, которые мы можем объединить, чтобы получить функцию f (a, b) -> (f a, f b). Составление с нашим pure из предыдущего дает (a, b) -> (f a, f b). Фух! Итак, напомним, у нас есть художественная диаграмма ASCII.

  (a, b) ---> f c
    |
    V
(f a, f b)

Теперь liftA2 дает нам функцию (f a, f b) -> f c, которую я не буду рисовать, потому что мне надоело строить ужасные диаграммы. Но дело в том, что диаграмма коммутирует, поэтому liftA2 фактически дает нам продолжение горизонтальной стрелки вдоль вертикальной.

«Подъем» много раз встречается в функциональном программировании, не только в fmap, но и во многих других контекстах. Примеры «лифтинга» включают:

• fmap :: (a -> b) -> F a -> F b где F - функтор
• cmap :: (b -> a) -> F a -> F b, где F - подрядчик
• bind :: (a -> M b) -> M a -> M b где M - монада
• ap :: F (a -> b) -> F a -> F b где F - аппликативный функтор
• point :: (_ -> a) -> _ -> F a где F - точечный функтор
• filtMap :: (a -> Maybe b) -> F a -> F b где F - фильтруемый функтор
• extend :: (M a -> b) -> M a -> M b, где M - комонада

Другие примеры включают аппликативный контрафунктор, фильтруемый контрафунктор и совмещенный функтор.

Все эти сигнатуры типов похожи в одном: они отображают один вид функции между a и b в другой вид функции между a и b.

В этих разных случаях типы функций не просто a -> b, но имеют какие-то «скрученные» типы: например, a -> M b или F (a -> b), или M a -> b, или F a -> F b и так далее. Однако каждый раз законы очень похожи: типы скрученных функций должны иметь законы идентичности и композиции, а скрученная композиция должна быть ассоциативной.

Например, для аппликативных функторов нам нужно уметь составлять функции типа F (a -> b). Итак, нам нужно определить специальную функцию «скрученной» идентичности (pure id :: F (a -> a)) и операцию «скрученной» композиции, назовите ее apcomp с сигнатурой типа F (a -> b) -> F (b -> c) -> F (a -> c). Эта операция должна иметь законы идентичности и ассоциативности. Операция ap должна иметь законы идентичности и композиции («карты искаженной идентичности в искаженную идентичность» и «карты искаженной композиции в искаженную композицию»).

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

Это потому, что мы можем сформулировать все эти операции как функторы в смысле теории категорий. Например, для аппликативного функтора мы определяем две категории: F-аппликативная категория (объекты a, b, ..., морфизмы F(a -> b)) и F-поднятая категория (объекты F a, F b, ..., морфизмы F a -> F b) . Функтор между этими двумя категориями требует от нас подъема морфизмов, ap :: F(a -> b) -> F a -> F b. Законы ap полностью эквивалентны стандартным законам этого функтора.

Подобные аргументы справедливы и для других классов типов. Нам необходимо определить категории, морфизмы, операции композиции, тождественные морфизмы и функторы в каждом случае. Убедившись, что законы выполняются, мы увидим, что каждый из этих классов типов имеет связанную пару категорий и функтор между ними, так что законы класса типов эквивалентны законам этих категорий и функтора.

Что мы получили? Мы сформулировали законы многих классов типов таким же образом (как законы категорий и функторов). Это великая экономия мысли: нам не нужно каждый раз запоминать все эти законы; мы можем просто запомнить, какие категории и какие функторы необходимо записать для каждого класса типов, при условии, что методы этого класса могут быть сведены к некоему «извилистому подъему».

Таким образом, мы можем сказать, что «лифтинги» важны и обеспечить применение теории категорий в функциональном программировании.

Я сделал презентацию об этом, https://www.youtube.com/watch?v=Zau8CxsfxOo, и я пишу новую бесплатную книгу, в которой будут показаны все производные. https://github.com/winitzki/sofp