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

Z Studia Informatyczne
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 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).