Vorlesung: Praxis der Funktionalen Programmierung
| Index
Rechenregeln für Monaden
Freie Theoreme
Damit ein Konstuktor eine Monade heißen darf,
muß er return und bind besitzen (siehe oben, das bind
wird als Operator >>= geschrieben),
und außerdem zunächst ein Funktor sein.
Damit gelten dann die "freien Theoreme"
für die Typen von return und bind:
return . f = fmap f . return
x >>= (g . f) = fmap f x >>= g
Wieso das? return :: a -> m a == Id a -> m a.
links steht also der identische Funktor
(dessen fmap ist ein id).
Aufgabe 1: erkläre genau, wie das freie Theorem für bind (>>=) entsteht.
Wir benötigen dazu eine instance Functor (c ->),
für jedes feste c, d. h. ein
fmap :: (a -> b) -> ((c -> a) -> (c -> b))
Was soll fmap f g bedeuten? Mit f :: a -> b und g :: c -> a
soll fmap f g :: c -> b sein. Wir wenden einfach auf das Resultat von g
die Funktion f an:
instance Functor ((->) c) where
fmap f g = f . g
Monaden-Axiome, Kleisli-Komposition
Für Monaden müssen zwei weitere Axiome gelten, damit return und bind
(vom passenden Typ) wirklich eine Monaden-Struktur erzeugen.
Diese Axiome drücken aus, daß die Nacheinanderausführung
von Rechnungen assoziativ ist,
und eine wirkungslose Rechnung eben nichts bewirkt.
Die genaue Formulierung bekommt man durch Kategorientheorie hergeleitet,
hier verstehen wir wenigstens das Resultat der Herleitung
durch Draufgucken.
Wir begeben uns zur eleganteren Beschreibung
in die Kleisli-Kategorie der Monade m,
d. h. die Pfeile haben alle den Typ a -> m b.
Dann betrachten wir statt bind die Kleisli-Komposition
(@@) :: (a -> m b) -> (b -> m c) -> (a -> m c)
f @@ g = \ x -> (f x) >>= g
Für diese muß gelten
f @@ (g @@ h) = (f @@ g) @@ h
return @@ f = f = f @@ return
Damit hat der Bereich (a -> m b) eine Monoid-Struktur:
assoziative Verknüpfung mit neutralem Element.
Beispiele
Wir wollen return @@ f = f für die Listen-Monade nachrechnen:
Zunächst bestimmen wir den Typ (beider Seiten), es ist ein a -> [ b ].
Wir wenden beide Seiten auf ein x :: a an und erhalten
f x =?= (return @@ f) x = return x >>= f
[ x ] >>= f = concat (map f [x]) = concat [ f x ] = f x
Und vielleicht noch f @@ (g @@ h) = (f @@ g) @@ h für Maybe:
Der Typ (beider Seiten) ist wieder a -> Maybe b,
wobei die einzelnen Bezeicher so aussehen (für geeignete c, d)
f :: a -> Maybe c; g :: c -> Maybe d; h :: d -> Maybe b
Wenden wir wieder beide Seiten auf ein x :: a an, erhalten wir
(f @@ (g @@ h)) x =?= (f @@ g) @@ h
f x >>= (g @@ h) =?= (f @@ g) x >>= h = (f x >>= g) >>= h
Betrachten wir den Fall f x = Nothing.
Dann kommt links und rechts Nothing heraus.
Wenn aber f x = Just y, dann
f x >>= (g @@ h) =?= (f @@ g) x >>= h = (f x >>= g) >>= h
Just y >>= (g @@ h) =?= (Just y >>= g) >>= h
(g @@ h) y =?= g y >>= h
und das ist genau die Definition von (@@).
Aufgabe 2
Wir schreiben f @@ return = f als Gleichung für (>>=),
indem wir beide Seiten auf ein x anwenden
f x = (f @@ return) x = f x >>= return
Unter Benutzung der do-Notation ist die rechte Seite
f x >>= return = do { z <- f x; return z }
Schreibe die andere Gleichung f = return @@ f ebenso.
Aufgabe 3
Die Funktor-Instanz einer Monade bekämen wir umsonst:
beweise aus den Monaden-Axiomen:
fmap f x = x >>= (return . f)
Aufgabe 4
Zum Üben wieder mal ein paar falsche Instanzen:
Welche der Axiome erfüllt
falsche-instance Monad Maybe where
return x = Nothing
(>>=) wie bei der richtigen Instanz
Finde eine falsche instance Monad [].
Sie soll sich "möglichst richtig" verhalten.
Aufgabe 5
Welche der bekannten Bäume
(binäre mit Schlüssel in Blättern, binär mit Schlüssel in inneren Knoten,
Rose Trees) lassen sich zu Monaden machen?
Nicht mit der Numerierung von früher verwechseln.
Dort ging es um Bäume, aber die Monade war eine Zustandsmonade.
Jetzt brauchen wir
instance Monad Tree where
return :: a -> Tree a
(>>=) :: Tree a -> (a -> Tree b) -> Tree b
Für (>>=) heißt das: aus jedem Schlüssel wird ein eigener Baum berechnet,
und diesen Baum von Bäumen müssen wir zu einem einzigen Baum zusammenkleben.
http://www.informatik.uni-leipzig.de/~joe/
mailto:joe@informatik.uni-leipzig.de