Teoria kategorii dla informatyków/Wykład 11: Monady: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Linia 1: Linia 1:
 +
 +
 
{{kotwica|wyklad11|}}
 
{{kotwica|wyklad11|}}
  
Linia 6: Linia 8:
 
==W poszukiwaniu kategorii algebraicznych==
 
==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'''.
+
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> ([[Teoria_kategorii_dla_informatyków/Wykład_5:_Funktory_i_transformacje_naturalne#mod5:def:konkret|Definicja 5.9]]). 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| ?]]
+
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 [[Teoria_kategorii_dla_informatyków/Wykład_9:_Sprzężenia_I#mod9:thm:adjtriangle|Twierdzenia 9.3]] dają nam następujące komutujące trójkąty:
dają nam następujące komutujące trójkąty:
 
  
\begin{diagram}
+
<center>[[Grafika:tk-11.1.png]]</center>
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| ?]]).
+
Naturalność <math>\varepsilon</math> daje dodatkowo komutujący diagram (Zadanie [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad1|Zadanie 11.1]]).
  
\begin{diagram}
+
<center>[[Grafika:tk-11.2.png]]</center>
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ć:
 
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:
+
{{definicja|11.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 \mu T = \mu \circ T\mu,</math></center>
Linia 45: Linia 38:
 
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
 
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}
+
<center>[[Grafika:tk-11.3.png]]</center>
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:
 
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}
+
<center>[[Grafika:tk-11.4.png]]</center>
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:
 
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:
Linia 68: Linia 53:
 
<center><math>F^{\mathbb{T}}(f\colon X\to Y):= Tf\colon (TX,\mu_X)\to (TY,\mu_Y).</math></center>
 
<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
+
W [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad2|Zadaniu 11.2]] 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/Ćwiczenia_11:_Monady#mod11:zad3|11.3]] udowodnimy, że
  
  
  
{{twierdzenie|6.2 [każda monada pochodzi od sprzężenia]|mod11:thm:EM|
+
{{twierdzenie|11.2 [każda monada pochodzi od sprzężenia]|mod11:thm:EM|
  
 
<center><math>F^{\mathbb{T}}\dashv G^{\mathbb{T}}</math></center>
 
<center><math>F^{\mathbb{T}}\dashv G^{\mathbb{T}}</math></center>
Linia 82: Linia 67:
  
 
* 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'''.
 
* 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>.
+
* 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 [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad5|Zadaniu 11.5]] 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| ?]].
+
* 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 [[Teoria_kategorii_dla_informatyków/Ćwiczenia_1:_Teoria_kategorii_jako_abstrakcyjna_teoria_funkcji#mod1:zad11|Zadaniu 1.11]]. Szczegóły tej konstrukcji opisujemy w [[Teoria_kategorii_dla_informatyków/Ćwiczenia_11:_Monady#mod11:zad6|Zadaniu 11.6]].
* 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
+
* Funktor <math>\mathrm{List}\colon \mathbf{Set}\to \mathbf{Mon}</math> z [[Teoria_kategorii_dla_informatyków/Wykład_5:_Funktory_i_transformacje_naturalne#mod5:ex:List|Przykładu 5.3]] 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>
 
<center><math>[[x_1,...,x_n],[y_1,...,y_m],...,[z_1,...,z_l]]</math></center>
Linia 107: Linia 92:
 
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:
 
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}
+
<nowiki>
 
class Monad m where
 
class Monad m where
 
     return :: a -> m a
 
     return :: a -> m a
 
     (>>=) :: m a -> (a -> m b) -> m b
 
     (>>=) :: m a -> (a -> m b) -> m b
\end{verbatim}
+
</nowiki>
  
 
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
 
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}
+
<nowiki>
 
map :: (t -> u) -> (M t -> M u)
 
map :: (t -> u) -> (M t -> M u)
\end{verbatim}
+
</nowiki>
  
 
zaś mnożenie monady jako
 
zaś mnożenie monady jako
  
\begin{verbatim}
+
<nowiki>
 
join :: M(Mt) -> Mt
 
join :: M(Mt) -> Mt
\end{verbatim}
+
</nowiki>
  
 
Wtedy mamy następującą listę zależności pomiędzy tymi operacjami:
 
Wtedy mamy następującą listę zależności pomiędzy tymi operacjami:
  
\begin{verbatim}
+
<nowiki> (map f) m</nowiki> jest tym samym, co:  <nowiki>m >>= (\x -> return (f x))</nowiki>
(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,
+
<nowiki>join m</nowiki> jest tym samym, co:  <nowiki>m >>= (\x -> x)</nowiki>
co:  join ((map f) m)
+
 
\end{verbatim}
+
<nowiki>m >>= f</nowiki>  jest tym samym, co:  <nowiki>join ((map f) m)</nowiki>

Wersja z 20:25, 18 sie 2006


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 . 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 (Definicja 5.9). Nawet, gdybyśmy dodatkowo zażądali, aby tenże funktor zapominania miał lewe sprzężenie , które wskazuje jak odbudować w sposób wolny zapomnianą strukturę, to sytuacja ciągle nie jest zadowalająca. Na przykład, funktor zapominania ma lewe sprzężenie a my nie chcemy traktować jako kategorii algebraicznej. Ale stąd warto rozpocząć poszukiwania, gdyż wszelkie kategorie, od których oczekujemy algebraiczności, jak czy posiadają lewe sprzężenia do funktorów zapominania, które przypisują zbiorom odpowiednie algebry wolne.

Niech zatem i będą sprzężone: . Rozważmy funktor będący złożeniem funktorów i : . Jedność sprzężenia ma zatem typ . Informacje o kojedności również nietrudno zakodować w terminach funktora , bowiem skoro , to (przypomnijmy definicję: ), a co za tym idzie: . Transformacja jest naturalna; jeśli oznaczymy ją jako , to dostajemy . Diagramy trójkątne charakteryzujące sprzężenie z Twierdzenia 9.3 dają nam następujące komutujące trójkąty:

Tk-11.1.png

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

Tk-11.2.png

Widzimy więc, że po wprowadzeniu endofunktora 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 nazywamy trójkę , gdzie jest funktorem, zaś i - tranformacjami naturalnymi takimi, że:

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


Uwaga
Dla sprzężenia , monada nazywa się monadą indukowaną przez . Jak każde pojęcie kategoryjne, monada ma swój odpowiednik dualny: komonadę. Każde sprzężenie indukuje komonadę .


Czy struktura monady nad kategorią zawsze pochodzi od pewnego sprzężenia? Zauważmy, że aby odpowiedzieć na to pytanie musimy przede wszystkim odnaleźć drugą kategorię i dwa funktory , , takie, że . 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 nad definiujemy -algebrę jako parę , gdzie , oraz

Tk-11.3.png

Morfizmem -algebr jest morfizm taki, że poniższy diagram komutuje:

Tk-11.4.png

Kategorię -algebr będziemy oznaczać . Nazywamy ją od nazwisk odkrywców: kategorią Eilenberga-Moore'a. Zobaczmy, że istnieje naturalny funktor zapominania definiowany jako:


Z drugiej strony, dla dowolnego , para jest tak zwaną wolną -algebrą, oznaczaną jako . Operacja rozszerza się do funktora , jeśli położymy:

W Zadaniu 11.2 pokażemy, że dla dowolnego jest rzeczywiście algebrą, zaś w Zadaniu następnym nr 11.3 udowodnimy, że


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

Monada indukowana przez to sprzężenie jest monadą .

Przykłady monad

  • Niech będzie częściowym porządkiem. Monadą nad jest funkcja monotoniczna taka, że oraz dla dowolnego . (Te dwie nierówności wyrażają typu transformacji i . Diagramy w definicji monady komutują, bo relacja jest przechodnia.) Powyższe zależności dla implikują, że , czyli . Funkcja jest więc idempotentna i traktuje się ją zwykle jako operację domknięcia.
  • Kowariantny funktor potęgowy indukuje monadę, gdzie jest zanurzeniem , zaś mnożenie jest sumą zbiorów: . 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 jest monadą nad . Identyczny dowód pokazuje, że (kowariantny funktor potęgowy na zbiorach skończonych) indukuje monadę nad .
  • Niech będzie monoidem. Funktor wraz z transformacjami naturalnymi oraz definiuje monadę . -algebry to -automaty, które poznaliśmy w Zadaniu 1.11. Szczegóły tej konstrukcji opisujemy w Zadaniu 11.6.
  • Funktor z Przykładu 5.3 jest lewym sprzężeniem do funktora zapominania . Złożenie jest funktorem, który zbiorowi przypisuje , będący zbiorem skończonych słów nad . Jedność jest oczywiście zanurzeniem elementu w listę jednoelementową . Jak zdefiniować mnożenie w tej monadzie? Jako proponujemy transformację naturalną, która liście list

przypisze listę

Łatwo pokazać, że jest monadą nad . Okazuje się, że kategoria -algebr jest równoważna z kategorią monoidów .

  • Rozważmy sprzężenie dla funktora wolnego i funktora zapominania . Niech będzie monadą indukowaną przez to sprzężenie. A zatem jest zbiorem podkładowym wolnej grupy nad zbiorem (czy Czytelnik pamięta z kursu algebry jak taka grupa jest tworzona?). Jeśli jest -algebrą, dostaniemy strukturę grupy na jeśli zdefiniujemy działanie jako , gdzie jest włożeniem generatorów, tzn. , , zaś jest mnożeniem w wolnej grupie nad . Za pomocą tej konstrukcji, dostajemy funktor . Odwrotnie, jeśli jest grupą, to homomorfizm , definiowany jako mnożenie liter słowa z za pomocą działania grupy , daje wraz z -algebrę , a zatem obiektową część funktora typu . Uwaga! Para funktorów, których szkic konstrukcji pokazaliśmy stanowi równoważność kategorii i .


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 jest algebraiczna, jeśli jest równoważna kategorii dla pewnej monady nad . 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)