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{𝐒}\mathbf{𝐞}\mathbf{𝐭}$. 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{𝐒}\mathbf{𝐞}\mathbf{𝐭}$ (Definicja 5.9). Nawet, gdybyśmy dodatkowo zażądali, aby tenże funktor zapominania $G:\mathbf{𝐂}\to \mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$ miał lewe sprzężenie $F⊣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{𝐓}\mathbf{𝐨}\mathbf{𝐩}\to \mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$ ma lewe sprzężenie, a my nie chcemy traktować $\mathbf{𝐓}\mathbf{𝐨}\mathbf{𝐩}$ jako kategorii algebraicznej. Ale stąd warto rozpocząć poszukiwania, gdyż wszelkie kategorie, od których oczekujemy algebraiczności, jak $\mathbf{𝐆}\mathbf{𝐫}\mathbf{𝐩}$ czy $\mathbf{𝐌}\mathbf{𝐨}\mathbf{𝐧}$, posiadają lewe sprzężenia do funktorów zapominania, które przypisują zbiorom odpowiednie algebry wolne.

Niech zatem $F:\mathbf{𝐂}\to \mathbf{𝐃}$ i $G:\mathbf{𝐃}\to \mathbf{𝐂}$ będą sprzężone: $F⊣G$. Rozważmy funktor $T:\mathbf{𝐂}\to \mathbf{𝐂}$ będący złożeniem funktorów $F$ i $G$: $T=GF$. Jedność $\eta :1_{\mathbf{𝐂}}\to GF$ sprzężenia ma zatem typ $1\to T$. Informacje o kojedności $\epsilon :FG\to 1_{\mathbf{𝐃}}$ również nietrudno zakodować w terminach funktora $T$, bowiem skoro $\epsilon :FG\to 1$, to ${\epsilon }_F:FGF\to F$ (przypomnijmy definicję: ${\epsilon }_F(-):={\epsilon }_{F(-)}$), a co za tym idzie: $G{\epsilon }_F:GFGF\to GF$. Transformacja $G{\epsilon }_F$ jest naturalna; jeśli oznaczymy ją jako $\mu$, to dostajemy $\mu :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ść $\epsilon$ 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{𝐂}$ nazywamy trójkę $\mathbb{𝕋}=(T,\eta ,\mu )$, gdzie $T:\mathbf{𝐂}\to \mathbf{𝐂}$ jest funktorem, zaś $\eta :1_{\mathbf{𝐂}}\to T$ i $\mu :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⊣G$, monada $(GF,\eta ,G{\eta }_F)$ nazywa się monadą indukowaną przez $F⊣G$. Jak każde pojęcie kategoryjne, monada ma swój odpowiednik dualny: komonadę. Każde sprzężenie indukuje komonadę $(FG,\epsilon ,F{\eta }_G)$.

Czy struktura monady $\mathbb{𝕋}=(T,\eta ,\mu )$ nad kategorią $\mathbf{𝐂}$ zawsze pochodzi od pewnego sprzężenia? Zauważmy, że aby odpowiedzieć na to pytanie musimy przede wszystkim odnaleźć drugą kategorię $\mathbf{𝐃}$ i dwa funktory $F:\mathbf{𝐂}\to \mathbf{𝐃}$, $G:\mathbf{𝐃}\to \mathbf{𝐂}$, $F⊣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,\eta ,\mu )$ nad $\mathbf{𝐂}$ definiujemy $\mathbb{𝕋}$-algebrę jako parę $(X,\theta )$, gdzie $X\in {\mathbf{𝐂}}_0$, $\theta :TX\to X$ oraz:

Morfizmem $\mathbb{𝕋}$-algebr $f:(X,\theta )\to (Y,\gamma )$ jest morfizm $f:X\to Y\in {\mathbf{𝐂}}_1$ taki, że poniższy diagram komutuje:

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

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

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

$F^{\mathbb{𝕋}}(f:X\to Y):=Tf:(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{𝕋}}⊣G^{\mathbb{𝕋}}$

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

Przykłady monad

• Niech $(P,\le )$ będzie częściowym porządkiem. Monadą nad $P$ jest funkcja monotoniczna $T:P\to P$ taka, że $x\le Tx$ oraz $TTx\le 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 $\le$ jest przechodnia.) Powyższe zależności dla $T$ implikują, że $Tx\le TTx$, czyli $TT=T$. Funkcja $T$ jest więc idempotentna i traktuje się ją zwykle jako operację domknięcia.
• Kowariantny funktor potęgowy ${𝒫}:\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}\to \mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$ indukuje monadę, gdzie ${\eta }_X:X\to {𝒫}(X)$ jest zanurzeniem ${\eta }_X(x)=\{x\}$, zaś mnożenie ${\mu }_X:{𝒫}{𝒫}(X)\to {𝒫}(X)$ jest sumą zbiorów: ${\mu }_X({𝒮})=\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 $({𝒫},\{\cdot \},\bigcup )$ jest monadą nad $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$. Identyczny dowód pokazuje, że ${{𝒫}}_{fin}:{\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}_{fin}\to {\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}_{fin}$ (kowariantny funktor potęgowy na zbiorach skończonych) indukuje monadę nad ${\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}_{fin}$.
• Niech $(M,*,e)$ będzie monoidem. Funktor $M\times (-):\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}\to \mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$ 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{𝕋}$. $\mathbb{𝕋}$-algebry to $M$-automaty, które poznaliśmy w Zadaniu 1.11. Szczegóły tej konstrukcji opisujemy w Zadaniu 11.6.
• Funktor $\mathrm{L}\mathrm{i}\mathrm{s}\mathrm{t}:\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}\to \mathbf{𝐌}\mathbf{𝐨}\mathbf{𝐧}$ z Przykładu 5.3 jest lewym sprzężeniem do funktora zapominania $U:\mathbf{𝐌}\mathbf{𝐨}\mathbf{𝐧}\to \mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$. 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 :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,\eta ,\mu )$ jest monadą nad $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$. Okazuje się, że kategoria $\mathbb{𝕋}$-algebr jest równoważna z kategorią monoidów $\mathbf{𝐌}\mathbf{𝐨}\mathbf{𝐧}$.

• Rozważmy sprzężenie $F⊣G$ dla funktora wolnego $F:\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}\to \mathbf{𝐆}\mathbf{𝐫}\mathbf{𝐩}$ i funktora zapominania $G:\mathbf{𝐆}\mathbf{𝐫}\mathbf{𝐩}\to \mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$. Niech $\mathbb{𝕋}$ 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{𝕋}$-algebrą, dostaniemy strukturę grupy na $X$, jeśli zdefiniujemy działanie jako $x\cdot y:=\theta (⟨x⟩⟨y⟩)$, gdzie $x\mapsto ⟨x⟩$ jest włożeniem generatorów, tzn. ${\eta }_X:X\to TX$, ${\eta }_X(x):=⟨x⟩$, zaś $⟨x⟩⟨y⟩$ jest mnożeniem w wolnej grupie nad $X$. Za pomocą tej konstrukcji dostajemy funktor ${\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}^{\mathbb{𝕋}}\to \mathbf{𝐆}\mathbf{𝐫}\mathbf{𝐩}$. Odwrotnie, jeśli $G$ jest grupą, to homomorfizm $f_G: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{𝕋}$-algebrę $(G,f_G)$, a zatem obiektową część funktora typu $\mathbf{𝐆}\mathbf{𝐫}\mathbf{𝐩}\to {\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}^{\mathbb{𝕋}}$. Uwaga! Para funktorów, których szkic konstrukcji pokazaliśmy, stanowi równoważność kategorii $\mathbf{𝐆}\mathbf{𝐫}\mathbf{𝐩}$ i ${\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}^{\mathbb{𝕋}}$.

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{𝐂}$ jest algebraiczna, jeśli jest równoważna kategorii ${\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}}^{\mathbb{𝕋}}$ dla pewnej monady $\mathbb{𝕋}$ nad $\mathbf{𝐒}\mathbf{𝐞}\mathbf{𝐭}$. 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).