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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m
 
Linia 1: Linia 1:
 
  
 
{{kotwica|wyklad11|}}
 
{{kotwica|wyklad11|}}
Linia 8: Linia 7:
 
==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> ([[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'''.
+
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 [[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:
 
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:
Linia 27: Linia 26:
 
<center><math>\mu \circ \eta_T = 1 = \mu\circ T\eta,</math></center>
 
<center><math>\mu \circ \eta_T = 1 = \mu\circ T\eta,</math></center>
  
tzn. takimi że powyższe trzy diagramy komutują.
+
tzn. takimi, że powyższe trzy diagramy komutują.
 
}}
 
}}
  
Linia 34: Linia 33:
  
  
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.
+
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
+
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:
  
 
<center>[[Grafika:tk-11.3.png]]</center>
 
<center>[[Grafika:tk-11.3.png]]</center>
Linia 44: Linia 43:
 
<center>[[Grafika:tk-11.4.png]]</center>
 
<center>[[Grafika:tk-11.4.png]]</center>
  
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 69: Linia 68:
 
* 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>.
 
* 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 [[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]].
 
* 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  [[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
+
* 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>
  
przypisze listę
+
przypisze 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>
  
 
Ł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>.
 
Ł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>.
+
* 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>.
  
  
Linia 90: Linia 89:
  
  
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:
  
 
<nowiki>
 
<nowiki>
Linia 98: Linia 97:
 
</nowiki>
 
</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:
  
<nowiki>
+
<nowiki>map :: (t -> u) -> (M t -> M u)</nowiki>,
map :: (t -> u) -> (M t -> M u)
 
</nowiki>
 
  
zaś mnożenie monady jako
+
zaś mnożenie monady jako:
  
<nowiki>
+
<nowiki>join :: M(Mt) -> Mt</nowiki>.
join :: M(Mt) -> Mt
 
</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:
  
<nowiki> (map f) m</nowiki>  jest tym samym, co:  <nowiki>m >>= (\x -> return (f x))</nowiki>  
+
<nowiki> (map f) m</nowiki>  jest tym samym, co:  <nowiki>m >>= (\x -> return (f x))</nowiki>,
  
<nowiki>join m</nowiki> jest tym samym, co:  <nowiki>m >>= (\x -> x)</nowiki>  
+
<nowiki>join m</nowiki> jest tym samym, co:  <nowiki>m >>= (\x -> x)</nowiki>,
  
<nowiki>m >>= f</nowiki>  jest tym samym, co:  <nowiki>join ((map f) m)</nowiki>
+
<nowiki>m >>= f</nowiki>  jest tym samym, co:  <nowiki>join ((map f) m)</nowiki>.

Aktualna wersja na dzień 12:12, 27 lis 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).