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

Z Studia Informatyczne
< Teoria kategorii dla informatyków
Wersja z dnia 10:12, 17 sie 2006 autorstwa Pqw (dyskusja | edycje)
(różn.) ← poprzednia wersja | przejdź do aktualnej wersji (różn.) | następna wersja → (różn.)
Przejdź do nawigacjiPrzejdź do wyszukiwania

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  ?). 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  ? 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ść daje dodatkowo komutujący diagram (Zadanie  ?).

\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 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]

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

\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 -algebr jest morfizm taki, że poniższy diagram komutuje:

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

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  ? pokażemy, że dla dowolnego jest rzeczywiście algebrą, zaś w Zadaniu następnym nr  ? udowodnimy, że


Twierdzenie 6.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  ? 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  ?. Szczegóły tej konstrukcji opisujemy w Zadaniu  ?.
  • Funktor z przykładu  ? 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:

\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}