W jaki sposób podnoszenie (w kontekście programowania funkcjonalnego) odnosi się do teorii kategorii?

Question

Patrząc na dokumentację Haskell, podnoszenie wydaje się zasadniczo uogólnieniem fmap, pozwalając na mapowanie funkcji z więcej niż jednym argumentem.

Artykuł na temat podnoszenia daje jednak odmienny pogląd, definiując "podniesienie" w kategoriach morfizmu w kategorii i jak odnosi się do innych obiektów i morfizmów w kategorii (nie podam szczegółów tutaj). Przypuszczam, że może to mieć znaczenie dla sytuacji Haskell, jeśli rozważamy Cat (kategorię kategorii, co czyni nasze funktory morfizmów), ale nie widzę, jak ta kategoria-teoretyczna koncepcja windy odnosi się do tej w Haskell. na podstawie połączonego artykułu, jeśli w ogóle to robi.

Jeśli te dwa pojęcia nie są tak naprawdę powiązane, a po prostu mają podobną nazwę, to czy dźwigi (teoria kategorii) używane są w ogóle w Haskell?

Answer 1

Dźwignie i podwójne pojęcie rozszerzeń są bezwzględnie używane w Haskell, być może najbardziej widocznym pod postacią komonady extend i monadycznej bind. (Mylące, extend jest winda, a nie rozszerzenie.) Komonada w 's pozwala nam podjąć funkcję w a -> b i podnieść go wzdłuż , aby uzyskać mapę. W sztuce ASCII, biorąc pod uwagę schemat

 w b 
     | 
     V 
w a ---> b 

gdzie strzałka pionowa jest wyciąg, extend daje nam ukośną strzałkę (co dojeżdżać schemat):

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

bardziej zaznajomieni z większością Haskellers jest podwójne pojęcie bind (>>=) dla monady m. Biorąc pod uwagę funkcję a -> m b i return :: a -> m a, możemy "rozszerzyć" naszą funkcję wzdłuż return, aby uzyskać funkcję m a -> m b. W sztuce ASCII:

a ---> m b 
| 
V 
m a 

daje nam

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

(To A jest grot!)

Więc tak, extend mogło być nazywane lift i bind mogło być nazywane extend. Jeśli chodzi o Haskella, lift, nie mam pojęcia, dlaczego tak się nazywają!

EDYCJA: Rzeczywiście, myślę, że znowu, Haskell's lift s są faktycznie rozszerzeniami. Jeśli f ma zastosowanie i mamy funkcję a -> b -> c, możemy skomponować tę funkcję z pure :: c -> f c, aby uzyskać funkcję a -> b -> f c. Uncurrying, to jest to samo co funkcja (a, b) -> f c. Teraz możemy również nacisnąć (a, b) z pure, aby uzyskać funkcję (a, b) -> f (a, b). Teraz, fmap ing i snd, otrzymujemy funkcje f (a, b) -> f a i f (a, b) -> f b, które możemy połączyć, aby uzyskać funkcję f (a, b) -> (f a, f b). Komponowanie z naszym pure z poprzedniej daje (a, b) -> (f a, f b). Uff!Przypomnę więc, mamy diagramu ASCII Art

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

Teraz liftA2 daje nam funkcję (f a, f b) -> f c, których nie będę rysować, bo jestem chory popełnienia strasznych diagramów. Chodzi jednak o to, że diagram się dojeżdża, więc faktycznie daje nam przedłużenie poziomej strzałki wzdłuż pionowej.