Tekst źródłowy strony Teoria kategorii dla informatyków/Wykład 11: Monady

{{kotwica|wyklad11|}}

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'' <math>\mathbf{Set}</math>. 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 <math>\mathbf{Set}</math> (Definicja [[Teoria_kategorii_dla_informatyków/TKI_Moduł_5#mod5:def:konkret| 5.?]]). Nawet, gdybyśmy dodatkowo zażądali, aby tenże funktor zapominania <math>G\colon \mathbf{C}\to \mathbf{Set}</math> miał lewe sprzężenie <math>F\dashv G</math>, które wskazuje jak odbudować w sposób wolny zapomnianą strukturę, to sytuacja ciągle nie jest zadowalająca. Na przykład, funktor zapominania <math>\mathbf{Top}\to \mathbf{Set}</math> ma lewe sprzężenie a my nie chcemy traktować <math>\mathbf{Top}</math> jako kategorii algebraicznej. Ale stąd warto rozpocząć poszukiwania, gdyż wszelkie kategorie, od których oczekujemy algebraiczności, jak <math>\mathbf{Grp}</math> czy <math>\mathbf{Mon}</math> posiadają lewe sprzężenia do funktorów zapominania, które przypisują zbiorom odpowiednie '''algebry wolne'''.

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

\begin{diagram}
T & \rTo^{\eta_T} & TT         & & & &  TT & \lTo^{T\eta} & T \\
  & \rdTo_{1_T}   & \dTo_{\mu} & & & &  \dTo^{\mu} & \ldTo_{1_T} & \\
  &               & T          & & & &  T & & \\
\end{diagram}

Naturalność <math>\varepsilon</math> daje dodatkowo komutujący diagram (Zadanie [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad1| ?]]).

\begin{diagram}
TTT & \rTo^{T\mu} & TT\\
\dTo^{\mu_T} & & \dTo_{\mu}\\
TT & \rTo_{\mu} & T\\
\end{diagram}

Widzimy więc, że po wprowadzeniu endofunktora <math>T</math> 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|6.1 [monada]|mod11:def:monada| '''Monadą''' w kategorii <math>\mathbf{C}</math> nazywamy trójkę <math>\mathbb{T} = (T,\eta,\mu)</math>, gdzie <math>T\colon\mathbf{C}\to\mathbf{C}</math> jest funktorem, zaś <math>\eta\colon 1_{\mathbf{C}}\to T</math> i <math>\mu\colon TT\to T</math> - tranformacjami naturalnymi takimi, że:

<center><math>\mu\circ \mu T = \mu \circ T\mu,</math></center>

<center><math>\mu \circ \eta_T = 1 = \mu\circ T\eta,</math></center>

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


{{uwaga||| Dla sprzężenia <math>F\dashv G</math>, monada <math>(GF,\eta,G\eta_F)</math> nazywa się '''monadą indukowaną przez''' <math>F\dashv G</math>. Jak każde pojęcie kategoryjne, monada ma swój odpowiednik dualny: komonadę. Każde sprzężenie indukuje komonadę <math>(FG,\varepsilon,F\eta_G)</math>.}}


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

\begin{diagram}
X & \rTo^{\eta_X} & TX & & & & TTX & \rTo^{\mu_X} & TX\\
&\rdTo^{1_X} & \dTo_{\theta} & & & & \dTo^{T\theta} & & \dTo_{\theta}\\
& & X & & & & TX & \rTo_{\theta} & X\\
\end{diagram}

Morfizmem <math>\mathbb{T}</math>-algebr <math>f\colon (X,\theta)\to (Y,\gamma)</math> jest morfizm <math>f\colon X\to Y\in \mathbf{C}_1</math> taki, że poniższy diagram komutuje:

\begin{diagram}
TX & \rTo^{Tf} & TY\\
\dTo^{\theta} & & \dTo_{\gamma}\\
X & \rTo_{f} & Y\\
\end{diagram}

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


<center><math>G^{\mathbb{T}}((X,\theta)\stackrel{f}{\to}(Y,\gamma)):= (X\stackrel{f}{\to}Y).</math></center>

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

<center><math>F^{\mathbb{T}}(f\colon X\to Y):= Tf\colon (TX,\mu_X)\to (TY,\mu_Y).</math></center>

W Zadaniu [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad2| ?]] pokażemy, że <math>(TX,\mu_X)</math> dla dowolnego <math>X</math> jest rzeczywiście algebrą, zaś w Zadaniu następnym nr [[Teoria_kategorii_dla_informatyków/TKI_Ćwiczenia_?#mod11:zad3| ?]] udowodnimy, że



{{twierdzenie|6.2 [każda monada pochodzi od sprzężenia]|mod11:thm:EM|

<center><math>F^{\mathbb{T}}\dashv G^{\mathbb{T}}</math></center>

Monada indukowana przez to sprzężenie jest monadą <math>\mathbb{T}</math>.
}}

==Przykłady monad==

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

<center><math>[[x_1,...,x_n],[y_1,...,y_m],...,[z_1,...,z_l]]</math></center>

przypisze listę

<center><math>[x_1,...,x_n,y_1,...,y_m,...,z_1,...,z_l].</math></center>

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


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 <math>\mathbf{C}</math> jest algebraiczna, jeśli jest równoważna kategorii <math>\mathbf{Set}^{\mathbb{T}}</math> dla pewnej monady <math>\mathbb{T}</math> nad <math>\mathbf{Set}</math>. 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: <math>>>=</math> i return:

\begin{verbatim}
class Monad m where
    return :: a -> m a
    (>>=) :: m a -> (a -> m b) -> m b
\end{verbatim}

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

\begin{verbatim}
map :: (t -> u) -> (M t -> M u)
\end{verbatim}

zaś mnożenie monady jako

\begin{verbatim}
join :: M(Mt) -> Mt
\end{verbatim}

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

\begin{verbatim}
(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)
\end{verbatim}