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

From Studia Informatyczne

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:

Grafika:tk-11.1.png

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

Grafika:tk-11.2.png

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:

Grafika:tk-11.3.png

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:

Grafika:tk-11.4.png

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).