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

Повдиганията и двойното понятие за разширения се използват абсолютно в Haskell, може би най-видно под прикритието на comonadic extend и monadic bind. (Объркващо е, че extend е повдигане, а не разширение.) extend на комонада w ни позволява да вземем функция 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

По-познато на повечето хаскелери е двойственото понятие 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, нямам представа защо се наричат ​​така!

РЕДАКТИРАНЕ: Всъщност мисля, че отново lifts на 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). Сега, като fmapизпълним 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