Teoria kategorii dla informatyków/Wykład 11: Monady

Ważną klasę kategorii tworzą takie, których obiektami są zbiory z pewną dodatkową strukturą algebraiczną, zaś morfizmami - funkcje, które tą strukturę zachowują. Takie kategorie moglibyśmy z powodzeniem nazwać kategoriami algebraicznymi nad $\mathbf {Set}$. Rozważania nad odpowiednią definicją algebraiczności doprowadzą nas do odkrycia ciekawej struktury kategoryjnej: monady, która jest niejako ukryta w każdym sprzężeniu między funktorami.

W poszukiwaniu kategorii algebraicznych

Z pewnością na kategorie algebraiczne nie nadają się wszystkie kategorie konkretne, które charakteryzują się tym, że posiadają funktor zapominania o kodziedzinie $\mathbf {Set}$ (Definicja 5.9). Nawet, gdybyśmy dodatkowo zażądali, aby tenże funktor zapominania $G\colon \mathbf {C} \to \mathbf {Set}$ miał lewe sprzężenie $F\dashv G$, które wskazuje jak odbudować w sposób wolny zapomnianą strukturę, to sytuacja ciągle nie jest zadowalająca. Na przykład, funktor zapominania $\mathbf {Top} \to \mathbf {Set}$ ma lewe sprzężenie, a my nie chcemy traktować $\mathbf {Top}$ jako kategorii algebraicznej. Ale stąd warto rozpocząć poszukiwania, gdyż wszelkie kategorie, od których oczekujemy algebraiczności, jak $\mathbf {Grp}$ czy $\mathbf {Mon}$, posiadają lewe sprzężenia do funktorów zapominania, które przypisują zbiorom odpowiednie algebry wolne.

Niech zatem $F\colon \mathbf {C} \to \mathbf {D}$ i $G\colon \mathbf {D} \to \mathbf {C}$ będą sprzężone: $F\dashv G$. Rozważmy funktor $T\colon \mathbf {C} \to \mathbf {C}$ będący złożeniem funktorów $F$ i $G$: $T=GF$. Jedność $\eta \colon 1_{\mathbf {C} }\to GF$ sprzężenia ma zatem typ $1\to T$. Informacje o kojedności $\varepsilon \colon FG\to 1_{\mathbf {D} }$ również nietrudno zakodować w terminach funktora $T$, bowiem skoro $\varepsilon \colon FG\to 1$, to $\varepsilon _{F}\colon FGF\to F$ (przypomnijmy definicję: $\varepsilon _{F}(-):=\varepsilon _{F(-)}$), a co za tym idzie: $G\varepsilon _{F}\colon GFGF\to GF$. Transformacja $G\varepsilon _{F}$ jest naturalna; jeśli oznaczymy ją jako $\mu$, to dostajemy $\mu \colon TT\to T$. Diagramy trójkątne charakteryzujące sprzężenie z Twierdzenia 9.3 dają nam następujące komutujące trójkąty:

Naturalność $\varepsilon$ daje dodatkowo komutujący diagram (Zadanie Zadanie 11.1).

Widzimy więc, że po wprowadzeniu endofunktora $T$ i prostym przekształceniu sprzężenia, od którego pochodzi, pojawiła się pewna struktura. Dobrze wyróżnić je definicją i dokładnie zbadać:

Definicja 11.1 [monada]

Monadą w kategorii $\mathbf {C}$ nazywamy trójkę $\mathbb {T} =(T,\eta ,\mu )$, gdzie $T\colon \mathbf {C} \to \mathbf {C}$ jest funktorem, zaś $\eta \colon 1_{\mathbf {C} }\to T$ i $\mu \colon TT\to T$ - tranformacjami naturalnymi takimi, że: $\mu \circ \mu T=\mu \circ T\mu ,$ $\mu \circ \eta _{T}=1=\mu \circ T\eta ,$

tzn. takimi, że powyższe trzy diagramy komutują.

Uwaga

Dla sprzężenia $F\dashv G$, monada $(GF,\eta ,G\eta _{F})$ nazywa się monadą indukowaną przez $F\dashv G$. Jak każde pojęcie kategoryjne, monada ma swój odpowiednik dualny: komonadę. Każde sprzężenie indukuje komonadę $(FG,\varepsilon ,F\eta _{G})$.

Czy struktura monady $\mathbb {T} =(T,\eta ,\mu )$ nad kategorią $\mathbf {C}$ zawsze pochodzi od pewnego sprzężenia? Zauważmy, że aby odpowiedzieć na to pytanie musimy przede wszystkim odnaleźć drugą kategorię $\mathbf {D}$ i dwa funktory $F\colon \mathbf {C} \to \mathbf {D}$, $G\colon \mathbf {D} \to \mathbf {C}$, $F\dashv G$ takie, że $T=GF$. Okazuje się, że odpowiedź jest pozytywna: każda monada pochodzi od pewnego sprzężenia, a tak naprawdę istnieje wiele sprzężeń indukujących daną monadę. Te sprzężenia tworzą oddzielną kategorię. My wskażemy obiekt końcowy tej kategorii.

Dla monady $\mathbb {T} =(T,\eta ,\mu )$ nad $\mathbf {C}$ definiujemy $\mathbb {T}$-algebrę jako parę $(X,\theta )$, gdzie $X\in \mathbf {C} _{0}$, $\theta \colon TX\to X$ oraz:

Morfizmem $\mathbb {T}$-algebr $f\colon (X,\theta )\to (Y,\gamma )$ jest morfizm $f\colon X\to Y\in \mathbf {C} _{1}$ taki, że poniższy diagram komutuje:

Kategorię $\mathbb {T}$-algebr będziemy oznaczać $\mathbf {C} ^{\mathbb {T} }$. Nazywamy ją od nazwisk odkrywców: kategorią Eilenberga - Moore'a. Zobaczmy, że istnieje naturalny funktor zapominania $G^{\mathbb {T} }\colon \mathbf {C} ^{\mathbb {T} }\to \mathbf {C}$ definiowany jako:

$G^{\mathbb {T} }((X,\theta ){\stackrel {f}{\to }}(Y,\gamma )):=(X{\stackrel {f}{\to }}Y).$

Z drugiej strony, dla dowolnego $X\in \mathbf {C} _{0}$, para $(TX,\mu _{X})$ jest tak zwaną wolną $\mathbb {T}$-algebrą, oznaczaną jako $F^{\mathbb {T} }(X)$. Operacja $F^{\mathbb {T} }$ rozszerza się do funktora $F^{\mathbb {T} }\colon \mathbf {C} \to \mathbf {C} ^{\mathbb {T} }$, jeśli położymy:

$F^{\mathbb {T} }(f\colon X\to Y):=Tf\colon (TX,\mu _{X})\to (TY,\mu _{Y}).$

W Zadaniu 11.2 pokażemy, że $(TX,\mu _{X})$ dla dowolnego $X$ jest rzeczywiście algebrą, zaś w Zadaniu następnym nr 11.3 udowodnimy, że

Twierdzenie 11.2 [każda monada pochodzi od sprzężenia]

$F^{\mathbb {T} }\dashv G^{\mathbb {T} }$

Monada indukowana przez to sprzężenie jest monadą $\mathbb {T}$.

Przykłady monad

• Niech $(P,\leq )$ będzie częściowym porządkiem. Monadą nad $P$ jest funkcja monotoniczna $T\colon P\to P$ taka, że $x\leq Tx$ oraz $TTx\leq Tx$ dla dowolnego $x\in P$. (Te dwie nierówności wyrażają typu transformacji $\eta$ i $\mu$. Diagramy w definicji monady komutują, bo relacja $\leq$ jest przechodnia.) Powyższe zależności dla $T$ implikują, że $Tx\leq TTx$, czyli $TT=T$. Funkcja $T$ jest więc idempotentna i traktuje się ją zwykle jako operację domknięcia.
• Kowariantny funktor potęgowy ${\mathcal {P}}\colon \mathbf {Set} \to \mathbf {Set}$ indukuje monadę, gdzie $\eta _{X}\colon X\to {\mathcal {P}}(X)$ jest zanurzeniem $\eta _{X}(x)=\{x\}$, zaś mnożenie $\mu _{X}\colon {\mathcal {P}}{\mathcal {P}}(X)\to {\mathcal {P}}(X)$ jest sumą zbiorów: $\mu _{X}({\mathcal {S}})=\bigcup \alpha$. Własności tej monady bardzo dobrze podsumowują teoriomnogościowe własności sumy w połączeniu z notacją $\{...\}$ służącą do konstrukcji zbiorów. W Zadaniu 11.5 przedstawiamy dowód, że $({\mathcal {P}},\{\cdot \},\bigcup )$ jest monadą nad $\mathbf {Set}$. Identyczny dowód pokazuje, że ${\mathcal {P}}_{fin}\colon \mathbf {Set} _{fin}\to \mathbf {Set} _{fin}$ (kowariantny funktor potęgowy na zbiorach skończonych) indukuje monadę nad $\mathbf {Set} _{fin}$.
• Niech $(M,*,e)$ będzie monoidem. Funktor $M\times (-)\colon \mathbf {Set} \to \mathbf {Set}$ wraz z transformacjami naturalnymi $\eta _{X}(x):=(e,x)$ oraz $\mu _{X}(m_{2}*(m_{1},x)):=(m_{2}*m_{1},x)$ definiuje monadę $\mathbb {T}$. $\mathbb {T}$-algebry to $M$-automaty, które poznaliśmy w Zadaniu 1.11. Szczegóły tej konstrukcji opisujemy w Zadaniu 11.6.
• Funktor $\mathrm {List} \colon \mathbf {Set} \to \mathbf {Mon}$ z Przykładu 5.3 jest lewym sprzężeniem do funktora zapominania $U\colon \mathbf {Mon} \to \mathbf {Set}$. Złożenie $T=UF$ jest funktorem, który zbiorowi $X$ przypisuje $T(X)$ będący zbiorem skończonych słów nad $X$. Jedność jest oczywiście zanurzeniem elementu $x\in X$ w listę jednoelementową $[x]$. Jak zdefiniować mnożenie w tej monadzie? Jako $\mu \colon TTX\to TX$ proponujemy transformację naturalną, która liście list:

$[[x_{1},...,x_{n}],[y_{1},...,y_{m}],...,[z_{1},...,z_{l}]]$

przypisze listę:

$[x_{1},...,x_{n},y_{1},...,y_{m},...,z_{1},...,z_{l}].$

Łatwo pokazać, że $\mathbb {T} =(T,\eta ,\mu )$ jest monadą nad $\mathbf {Set}$. Okazuje się, że kategoria $\mathbb {T}$-algebr jest równoważna z kategorią monoidów $\mathbf {Mon}$.

• Rozważmy sprzężenie $F\dashv G$ dla funktora wolnego $F\colon \mathbf {Set} \to \mathbf {Grp}$ i funktora zapominania $G\colon \mathbf {Grp} \to \mathbf {Set}$. Niech $\mathbb {T}$ będzie monadą indukowaną przez to sprzężenie. A zatem $T(X)$ jest zbiorem podkładowym wolnej grupy nad zbiorem $X$ (czy Czytelnik pamięta z kursu algebry, jak taka grupa jest tworzona?). Jeśli $(X,\theta )$ jest $\mathbb {T}$-algebrą, dostaniemy strukturę grupy na $X$, jeśli zdefiniujemy działanie jako $x\cdot y:=\theta (\langle x\rangle \langle y\rangle )$, gdzie $x\mapsto \langle x\rangle$ jest włożeniem generatorów, tzn. $\eta _{X}\colon X\to TX$, $\eta _{X}(x):=\langle x\rangle$, zaś $\langle x\rangle \langle y\rangle$ jest mnożeniem w wolnej grupie nad $X$. Za pomocą tej konstrukcji dostajemy funktor $\mathbf {Set} ^{\mathbb {T} }\to \mathbf {Grp}$. Odwrotnie, jeśli $G$ jest grupą, to homomorfizm $f_{G}\colon F(G)\to G$, definiowany jako mnożenie liter słowa z $F(G)$ za pomocą działania grupy $G$, daje wraz z $G$ $\mathbb {T}$-algebrę $(G,f_{G})$, a zatem obiektową część funktora typu $\mathbf {Grp} \to \mathbf {Set} ^{\mathbb {T} }$. Uwaga! Para funktorów, których szkic konstrukcji pokazaliśmy, stanowi równoważność kategorii $\mathbf {Grp}$ i $\mathbf {Set} ^{\mathbb {T} }$.

Dwa ostatnie przykłady wskazują nam to, czego szukaliśmy od początku wykładu: odpowiedzi na pytanie, jakie kategorie chcemy uważać za algebraiczne!

Uwaga

Slogan: Kategoria $\mathbf {C}$ jest algebraiczna, jeśli jest równoważna kategorii $\mathbf {Set} ^{\mathbb {T} }$ dla pewnej monady $\mathbb {T}$ nad $\mathbf {Set}$. W ten sposób algebraiczne są grupy, grupy abelowe, monoidy, pierścienie, algebry Boole'a, półkraty, zwarte przestrzenie Hausdorffa. Przykładem kategorii, która nie jest algebraiczna są zupełne algebry Boole'a.

Monady w Haskellu

Monady są wykorzystywane m.in. w funkcyjnym języku programowania Haskell. Struktura monady doskonale nadaje się do specyfikacji: (a) operacji wejścia/wyjścia; (b) wyłapywania wyjątków (takich jak np. dzielenie przez zero); (c) interfejsów graficznych. Formalnie, monada w Haskellu jest pewnym typem danych, bardzo czytelnie opisuje tę sytuację w przypadku monady I/O (wejścia/wyjścia) fragment wykładu Paradygmaty programowania. Tenże Haskellowy typ danych jest tak naprawdę inastancją klasy Monad. Ta klasa wyposażona jest zawsze w dwie funkcje: $>>=$ i return:

class Monad m where return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b

Funkcja return oczywiście pełni rolę jedności monady, zaś operacja >>= zawiera całą informację o funktorze indukującym monadę i mnożeniu. Dokładniej mówiąc, funktor indukujący monadę oznacza się jako:

map :: (t -> u) -> (M t -> M u),

zaś mnożenie monady jako:

join :: M(Mt) -> Mt.

Wtedy mamy następującą listę zależności pomiędzy tymi operacjami:

(map f) m jest tym samym, co: m >>= (\x -> return (f x)),

join m jest tym samym, co: m >>= (\x -> x),

m >>= f jest tym samym, co: join ((map f) m).