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

Глядя на документацию Haskell, подъем, по-видимому, в основном представляет собой обобщение fmap, позволяющее отображать функции с более чем одним аргументом.

Wikipedia статья о подъеме дает другое представление, однако, определяя "подъем" в терминах морфизма в категории и как оно относится к другие объекты и морфизмы в категории (здесь я не буду приводить подробностей). Я полагаю, что это может иметь отношение к ситуации Хаскелла, если мы рассматриваем Cat (категорию категорий, что делает наши функторы морфизмов), но я не вижу, как это категориальное понятие лифта относится к такому в Haskell на основе связанной статьи, если это вообще происходит.

Если две концепции не связаны друг с другом и имеют простое имя, это лифты (теория категорий), используемые в Haskell вообще?

Ответы

Ответ 1

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

        w b
         |
         V
w a ---> b

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

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

Более знакомым большинству Haskellers является двойное понятие 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. ~~Что касается Haskell lift s, я понятия не имею, почему они называются так!~~

EDIT: На самом деле, я думаю, что снова Haskell lift на самом деле являются расширениями. Если f является аппликативным, и мы имеем функцию a -> b -> c, мы можем скомпоновать эту функцию с pure :: c -> f c, чтобы получить функцию a -> b -> f c. Uncurrying, это то же самое, что и функция (a, b) -> f c. Теперь мы можем также нажать (a, b) с помощью pure, чтобы получить функцию (a, b) -> f (a, b). Теперь, fmap ing 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 art

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

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