Monade (Informatik)

Grundidee und Bedeutung

Eine Monade ist in der funktionalen Programmierung ein abstrakter Datentyp, mit dem Berechnungen strukturiert und miteinander verknüpft werden. Sie ist besonders wichtig für Sprachen ohne Nebeneffekte: Dort können Fehler, Zustandsänderungen oder Ein-/Ausgaben nicht einfach wie in imperativen Sprachen nebenbei stattfinden, sondern müssen als Teil des Berechnungstyps dargestellt werden.

Eine Computerberechnung liefert daher nicht unbedingt nur einen „reinen“ Wert. Typische Möglichkeiten sind:

• Maybe: kein Wert oder genau ein Wert,
• Either: ein Fehlerwert oder ein Berechnungswert,
• List: kein, ein oder mehrere Ergebnisse, etwa zur Modellierung von Nichtdeterminismus,
• State: ein Ergebnis zusammen mit einem zu berücksichtigenden Systemzustand,
• IO: Ein- und Ausgabeoperationen.

Monaden können außerdem gewöhnliche Behälter wie Listen oder Mengen beschreiben, ohne dass man sie als Effekte deuten muss. Ihre Struktur und ihre Gesetze sorgen dafür, dass sich solche Berechnungen konsistent zusammensetzen lassen.

Eine zentrale Rolle spielt der Typkonstruktor M. Er erzeugt aus einem zugrunde liegenden Typ A den „höheren“ Typ M A. Ein höherer Typ benötigt mindestens einen Typparameter, bevor ein konkreter Typ entsteht. So wird aus List und Int der Typ List(Int). Die Signatur sum : List(Int) → Int beschreibt eine Funktion, die eine Liste ganzer Zahlen summiert. Dagegen funktioniert length : List(A) → Int unabhängig vom Elementtyp A. Der Doppelpunkt kennzeichnet eine Typsignatur; links vom Pfeil steht die Eingabe, rechts das Ergebnis.

Das Konzept stammt aus der Kategorientheorie. Dort untersucht man mathematische Objekte und ihre Beziehungen mithilfe von Morphismen und Funktoren. In der Programmierung übertragen Monaden Werte und Funktionen von einfachen Typen auf monadische Typen und fassen mehrere solcher Schritte zu einer Gesamtberechnung zusammen.

Bestandteile und Operationen

Eine Monade besitzt einen Typkonstruktor M und eine Einheitsfunktion return. Für jeden Typ A ist M A der zugehörige monadische Typ. Bei der Listenmonade ist M gleich List und M A somit List A. Der Typ A darf selbst bereits zusammengesetzt sein, beispielsweise List B.

Die grundlegenden Operationen sind:

• return : A → M A hebt einen reinen Wert in den monadischen Typ. Bei Listen entsteht eine einelementige Liste.
• join : M (M A) → M A entfernt eine Verschachtelungsebene. Bei Listen wird beispielsweise eine Liste von Listen zu einer einfachen Liste abgeflacht.
• fmap : (A → B) → M A → M B überträgt eine gewöhnliche Funktion auf den monadischen Typ. Eine Funktion von Int nach String kann so auf alle Elemente einer List Int angewandt werden und eine List String erzeugen.
• bind mit >>= : M A → (A → M B) → M B verknüpft eine monadische Berechnung mit einer Funktion, die aus einem reinen A eine neue monadische Berechnung M B erzeugt.
• Der Kleisli-Operator >=> : (A → M B) → (B → M C) → (A → M C) komponiert zwei Funktionen, die monadische Ergebnisse liefern.

Eine an der Kategorientheorie orientierte Definition versteht M als Endofunktor, also als Funktor von einer Kategorie in dieselbe Kategorie. Dazu gehören fmap sowie die natürlichen Transformationen return und join. bind lässt sich daraus definieren als ma >>= f = (join ∘ (fmap f)) ma. Eine natürliche Transformation ist dabei eine strukturverträgliche Abbildung zwischen Funktoren.

In Haskell genügt üblicherweise die Definition von return und >>=: return :: a -> m a (>>=) :: m a -> (a -> m b) -> m b

Dann gelten (f >=> g) a = f a >>= g, fmap f ma = ma >>= (return . f) und join mma = mma >>= id. Alternativ kann man eine Monade durch return und >=> oder, analog zur Kategorientheorie, durch fmap, return und join festlegen. Jede dieser Varianten erlaubt es, die jeweils übrigen Operationen abzuleiten. In Agda können die geforderten Gesetze zusammen mit der Definition formal bewiesen werden; Haskell verlangt solche Beweise im Typsystem nicht.

Jede Monade ist auch ein applikativer Funktor und damit ein Funktor, aber nicht jeder Funktor oder applikative Funktor ist eine Monade. Diese Hierarchie wurde im Glasgow Haskell Compiler mit Version 7.10 ausdrücklich in der Standardbibliothek abgebildet.

Gesetze für korrekte Verknüpfungen

Monadengesetze sichern, dass verschiedene, strukturell gleichwertige Zusammensetzungen dasselbe Ergebnis liefern. Da M ein Funktor ist, gelten zunächst die Funktorgesetze:

fmap id ≡ id fmap (f ∘ g) ≡ (fmap f) ∘ (fmap g)

Das erste Gesetz besagt, dass die Übertragung der Identitätsfunktion nichts verändert. Das zweite besagt, dass die Übertragung einer zusammengesetzten Funktion dasselbe ergibt wie die nacheinander ausgeführten Übertragungen.

Für return und join gelten Natürlichkeitsbedingungen:

(fmap f) ∘ return ≡ return ∘ f (fmap f) ∘ join ≡ join ∘ ((fmap ∘ fmap) f)

Somit spielt es keine Rolle, ob eine passende Funktion vor oder nach dem Einbetten beziehungsweise Abflachen angewandt wird.

Die Monadenaxiome für join und return umfassen insbesondere:

join ∘ (fmap join) ≡ join ∘ join join ∘ return ≡ id join ∘ (fmap return) ≡ id

Die erste Gleichung ist ein Assoziativgesetz für mehrfach verschachtelte monadische Werte. Die beiden anderen drücken aus, dass return beim anschließenden Abflachen neutral wirkt.

Für bind lautet die Assoziativität: (ma >>= f) >>= g ≡ ma >>= (λ a → ((f a) >>= g))

return ist dabei links und rechts neutral: ma >>= return ≡ ma (return a) >>= f ≡ f a

Auch der Kleisli-Operator ist assoziativ, und return ist sein Neutralelement: ((f >=> g) >=> h) a ≡ (f >=> (g >=> h)) a (f >=> return) a ≡ (return >=> f) a ≡ f a

Die Gesetze von bind und >=> lassen sich aus den Gesetzen für fmap, return und join ableiten. In Sprachen mit entsprechend starkem Typsystem können sie formal bewiesen werden; in Haskell werden sie als einzuhaltende Eigenschaften beziehungsweise Eigenschaftstests behandelt.

Eine allgemeine Funktion extract : M A → A existiert nicht für beliebige Endofunktoren M. join entfernt lediglich eine monadische Verschachtelung; der Wert bleibt monadisch. Nur besondere Monaden können eine passende Extraktionsfunktion besitzen.

Typische Berechnungen und Listen

Haskell und Agda erleichtern monadische Verkettungen durch die do-Notation. Die Schreibweise x ← ma entnimmt dabei nicht allgemein einen Wert aus der Monade, sondern ist syntaktischer Zucker für bind.

Bei Maybe können weitere Berechnungsschritte mit x und y formuliert werden, ohne jedes Mal zwischen just und nothing unterscheiden zu müssen. Im Artikel ergibt eine Berechnung aus return 3 und return 5 den Wert just 53. In einem zweiten Beispiel wird geprüft, ob x plus die Länge einer Liste höchstens 6 ist. Ist die Bedingung erfüllt, wird weitergerechnet; kommt noch ein Element zur Liste hinzu, lautet das Gesamtergebnis nothing. Die Fehler- beziehungsweise Abbruchbehandlung wird somit durch die Maybe-Monade weitergegeben.

Bei der Listenmonade steht jede Eingabeliste für mehrere mögliche Werte. Die Berechnung x ← [1,2,3] y ← [7,8,9,10] return (x + 3 * y)

erzeugt alle Kombinationen und liefert [22,25,28,31,23,26,29,32,24,27,30,33]. bind wendet die übergebene Funktion auf jedes Listenelement an und verbindet die entstehenden Teillisten durch Listenverkettung. return a = [a], fmap entspricht map und join entspricht concat. Allgemeiner funktionieren Mengen und Multimengen ähnlich; ihre Ergebnisse werden durch Mengen- beziehungsweise Multimengenvereinigung zusammengeführt.

Die ausführliche Agda-Formalisierung konstruiert zunächst List als Funktor mit map als Morphismenabbildung. Die Funktorgesetze werden durch Fallunterscheidung über [] und x ∷ xs bewiesen. Danach werden return als x ∷ [] und join als concat definiert. Auch Natürlichkeit, Assoziativität sowie linke und rechte Identität werden formal bewiesen. Erst danach wird bind aus join und fmap aufgebaut. Unit-Tests bestätigen für zwei Beispielprogramme exakt die erwarteten Ergebnislisten. Die Formalisierung zeigt, dass Agda nicht nur die Anwendung, sondern auch den maschinengeprüften Nachweis der Monadengesetze ermöglicht.

Auch Ein- und Ausgabe wird monadisch modelliert. Ein Programm kann eine Aufforderung ausgeben, mit getLine einen Namen lesen und anschließend „Hallo “ mit dem Namen ausgeben. Der Ergebnistyp IO ⊤ verwendet den Einheitstyp ⊤ mit seinem einzigen Konstruktor tt.

Die Identitätsmonade beschreibt reine mathematische Berechnungen ohne zusätzlichen Behälter. Hier bleibt der Typ unverändert: return : a -> a, fmap : (a -> b) -> a -> b und join : a -> a. Es gelten return x = x, join x = x und fmap f x = f x. bind ist damit gewöhnliche Funktionsanwendung beziehungsweise Hintereinanderausführung. Im Beispiel ergibt die Kombination von 4 und 5 durch x + 3*y den Wert 19. Dadurch kann dieselbe Berechnungsstruktur zunächst mit einfachen Werten erprobt und später mit einer anderen Monade verwendet werden.

Zustände, Vektoren und Sprachunterstützung

Die State-Monade modelliert veränderlichen Zustand in einer reinen funktionalen Sprache, indem jede Berechnung den alten Zustand als Argument erhält und den neuen Zustand zusammen mit dem Ergebnis zurückgibt. Der zugehörige Typ lautet: State S A = S → S × A

S ist der Zustandstyp, A der Ergebnistyp. Für jeden Zustandstyp S entsteht damit eine eigene Monade. getState : State S S liefert den Zustand sowohl als neuen Zustand als auch als Ergebnis. putState : S → State S ⊤ ersetzt den bisherigen Zustand und liefert tt. Die Einheitsfunktion return : A → State S A lässt den Zustand unverändert und gibt den reinen Wert zurück.

bind reicht den Zwischenzustand automatisch an den nächsten Schritt weiter. Im Beispiel liest ein Programm einen Zähler, erhöht ihn mit putState und gibt die Verkettung zweier Zeichenketten zurück. Der Aufruf mit „hallo“, „welt“ und dem Anfangszustand 10 ergibt (11, "hallowelt"). In do-Notation wirkt der Zähler ähnlich wie eine veränderliche globale Variable, obwohl er tatsächlich kontrolliert durch die Funktionen weitergereicht wird. Die ausgeschriebene Fassung mit verschachtelten bind-Aufrufen ist deutlich komplexer und verdeutlicht den Nutzen der do-Notation.

Ein weiteres Beispiel verwendet Vektorräume. Der Typkonstruktor bildet T auf einen Vektorraum V(T) ab, dessen Basis durch T bezeichnet wird. bind hat den Typ V(T) → (T → V(U)) → V(U). Nach Vertauschen der Argumente erkennt man (T → V(U)) → (V(T) → V(U)): Eine auf Basiselementen definierte Funktion wird zu einer vollständigen linearen Abbildung erweitert. return bildet ein Basiselement auf den entsprechenden Basisvektor ab.

Andere Programmiersprachen bieten verwandte Schreibweisen. C#-LINQ-Abfrageausdrücke sind von Haskells do-Notation inspiriert und werden in Aufrufe der Methoden Select und SelectMany übersetzt. Eine Haskell entsprechende Typklasse Monad lässt sich in C# jedoch nicht ausdrücken. Scala verwendet für for-Comprehensions die Methoden map und flatMap. In Java 8 besitzen mindestens Optional und Stream die monadentypischen Methoden map, flatMap und of.