Wir haben in verschiedenen Kontexten immer wieder die gleichen Funktionen kennengelernt. In diesem Kapitel wollen wir uns ein wenig den Hintergrund hinter diesen Funktionen anschauen. Die Konzepte, die wir in diesem Kapitel lernen, sind vergleichbar mit Pattern in objektorientierten Sprachen. Das heißt, man identifiziert Funktionen, die man für verschiedene Datenstrukturen definieren kann und beschreibt, welche Eigenschaften diese Funktionen haben sollten.

You say "pattern" and nobody panics, you say "monad" and everybody is losing their mind

Funktoren

Wir haben die Funktion map kennengelernt, die auf vielen verschiedenen Datentypen definiert werden kann. Wir haben zum Beispiel die folgenden Funktionen kennengelernt.

map : (a -> b) -> List    a -> List    b
map : (a -> b) -> Html    a -> Html    b
map : (a -> b) -> Decoder a -> Decoder b

Diese Signaturen unterschieden sich nur in dem Typkonstruktor, für den sie definiert sind. Das heißt, es gibt eine Definition von map für den Typkonstruktor List, eine Definition für den Typkonstruktor Html und eine Definition für den Typkonstruktor Decoder. Das heißt, die Funktion map hat immer die Form

map : (a -> b) -> f a -> f b

wobei f ein Typkonstruktor ist.

Wichtig

Man bezeichnet einen Typkonstruktor f, für den es eine Funktion map gibt, als Funktor.

Es gibt noch viele weitere Typkonstruktoren, für die wir eine Funktion map definieren können. Neben den Implementierungen von map, die wir kennengelernt haben, gibt es in den Standardbibliotheken von Elm zum Beispiel noch die folgenden Funktionen.

map : (a -> b) -> Cmd      a -> Cmd      b
map : (a -> b) -> Sub      a -> Sub      b
map : (a -> b) -> Result x a -> Result x b

Zur Illustration wollen wir eine weitere Variante der Funktion map definieren, dieses Mal für den Typkonstruktor Maybe.

map : (a -> b) -> Maybe a -> Maybe b
map func maybeValue =
    case maybeValue of
        Nothing ->
            Nothing

        Just value ->
            Just (func value)

Die obige Implementierung der Funktion map für Maybe ist aber nicht die einzige mögliche Implementierung. Wir können zum Beispiel die folgende Funktion vom Typ (a -> b) -> Maybe a -> Maybe b definieren, die keine “sinnvolle” Implementierung darstellt.

mapWeird : (a -> b) -> Maybe a -> Maybe b
mapWeird _ _ =
    Nothing

Um solche Implementierungen zu vermeiden, sollte die Implementierung der Funktion map für jeden Typkonstruktor bestimmte Gesetze erfüllen. Das heißt, die Funktion muss den angegebenen Typ haben und sich auf gewisse Weise verhalten. Die Funktion map sollte für alle möglichen Werte für fx, f und g die folgenden beiden Gesetze erfüllen.

map (\x -> x) fx = fx
map f (map g fx) = map (\x -> f (g x)) fx

Die Funktion mapWeird erfüllt zum Beispiel das erste Gesetz nicht, da für fx = Just 42 die erste Gleichung nicht erfüllt ist, wie die folgenden Umformungen illustrieren.

mapWeird (\x -> x) fx
  • = 
    mapWeird (\x -> x) (Just 42)

    Definition von fx

  • = 
    Nothing

    Definition von mapWeird

  • ≠ 
    Just 42
  • = 
    fx

    Definition von fx

Wichtig

Diese Form der Argumentation über das Verhalten von funktionalen Programmen bezeichnet man als equational reasoning.

In einer referenziell transparenten Programmiersprache kann man den Aufruf einer Funktion durch die Definition ersetzen. Es handelt sich dabei um eine mathematische Gleichheit. Bei Programmiersprachen mit Seiteneffekten ist eine solche gleichheitsbasierte Umformung nur möglich, wenn die Seiteneffekte ebenfalls berücksichtigt werden. Dies ist zwar möglich, aber sehr aufwendig.

Die Gesetze für Abstraktionen wie Funktoren und Monaden sind Allaussagen. Daher ist es vergleichsweise einfach zu zeigen, dass eine Implementierung ein Gesetz nicht erfüllt. Wir müssen dazu lediglich ein Gegenbeispiel angeben. Um zu zeigen, dass eine Funktion ein Gesetz erfüllt, müssen wir eine Allaussage beweisen. Der Beweis einer Allaussage ist im Vergleich zur Widerlegung einer Allaussage vergleichsweise schwierig. Bevor wir mit einem solchen Beweis starten, überprüfen wir, ob das Gegenbeispiel für mapWeird auch ein Gegenbeispiel für die Funktion Maybe.map ist.

Maybe.map (\x -> x) fx
  • = 
    Maybe.map (\x -> x) (Just 42)

    Definition von fx

  • = 
    case Just 42 of
    Nothing ->
        Nothing

    Just value ->
        Just ((\x -> x) value)

    Definition von Maybe.map

  • = 
    Just ((\x -> x) 42)

    Auswertung des case-Ausdrucks

  • = 
    Just 42

    Anwendung des Lambda-Ausdrucks

  • = 
    fx

    Definition von fx

Diese Umformung zeigt, dass Just 42 kein Gegenbeispiel die Funktion Maybe.map ist. Wir haben damit nicht gezeigt, dass die Funktion Maybe.map das Gesetz erfüllt. Um zu zeigen, dass eine Implementierung ein Gesetz erfüllt, müssen wir einen Beweis führen.

Sei t ein Typ. Sei fx vom Typ Maybe t. Wir betrachten den Ausdruck Maybe.map (\x -> x) fx. Wir führen eine Fallunterscheidung über fx durch.

  1. Wir betrachten den Fall fx = Nothing

    Maybe.map (\x -> x) fx
    • = 
      Maybe.map (\x -> x) Nothing

      Definition von fx

    • = 
      case Nothing of
    Nothing ->
        Nothing

    Just value ->
        Just ((\x -> x) value)

      Definition von Maybe.map

    • = 
      Nothing

      Auswertung des case-Ausdrucks

    • = 
      fx

      Definition von fx

  2. Wir betrachten den Fall fx = Just x

    Maybe.map (\x -> x) fx
    • = 
      Maybe.map (\x -> x) (Just x)

      Definition von fx

    • = 
      case Just x of
    Nothing ->
        Nothing

    Just value ->
        Just ((\x -> x) value)

      Definition von Maybe.map

    • = 
      Just ((\x -> x) x)

      Auswertung des case-Ausdrucks

    • = 
      Just x

      Auswertung des case-Ausdrucks

    • = 
      fx

      Definition von fx

Das heißt, dass in allen Fällen map (\x -> x) fx = fx gilt. Damit haben wir bewiesen, dass die Funktion Maybe.map das erste Funktorgesetz erfüllt. Wir ignorieren an dieser Stelle, dass die Auswertung von fx einen Fehler liefern oder nicht terminieren könnte. Wenn wir formal korrekt arbeiten möchten, müssten wir diesen Fall ebenfalls berücksichtigen. Der Einfachheit halber ignorieren wir hier aber, dass die Auswertung eines Ausdrucks einen Fehler liefern oder nicht terminieren könnte.

Wir betrachten als nächstes das zweite Funktorgesetz. Seien t1, t2, t3 Typen. Sei f vom Typ t2 -> t3. Sei g vom Typ t1 -> t2 Sei fx vom Typ Maybe t1. Wir betrachten den Ausdruck Maybe.map f (Maybe.map g fx). Wir führen eine Fallunterscheidung über fx durch.

  1. Wir betrachten den Fall fx = Nothing

    Maybe.map f (Maybe.map g fx)
    • = 
      Maybe.map f (Maybe.map g Nothing)

      Definition von fx

    • = 
      Maybe.map f (case Nothing of
                 Nothing ->
                     Nothing

                 Just value ->
                     Just (g value))

      Definition von Maybe.map

    • = 
      Maybe.map f Nothing

      Auswertung des case-Ausdrucks

    • = 
      case Nothing of
    Nothing ->
        Nothing

        Just value ->
            Just (f value)

      Definition von Maybe.map

    • = 
      Nothing

    Für die andere Seite der Gleichung argumentieren wir wie folgt.

    Maybe.map (\x -> f (g x)) fx
    • = 
      Maybe.map (\x -> f (g x)) Nothing

      Definition von fx

    • = 
      case Nothing of
    Nothing ->
        Nothing

    Just value ->
        Just ((\x -> f (g x)) value))

      Definition von Maybe.map

    • = 
      Nothing

  2. Wir betrachten den Fall fx = Just x

    Maybe.map f (Maybe.map g fx)
    • = 
      Maybe.map f (Maybe.map g (Just x))

      Definition von fx

    • = 
      Maybe.map f (case Just x of
                 Nothing ->
                     Nothing

                 Just value ->
                     Just (g value))

      Definition von Maybe.map

    • = 
      Maybe.map f (Just (g x))

      Auswertung des case-Ausdrucks

    • = 
      case Just (g x) of
    Nothing ->
        Nothing

        Just value ->
            Just (f value))

      Definition von Maybe.map

    • = 
      Just (f (g x))

      Definition von fx

    Für die andere Seite der Gleichung argumentieren wir wie folgt.

    Maybe.map (\x -> f (g x)) fx
    • = 
      Maybe.map (\x -> f (g x)) (Just x)

      Definition von fx

    • = 
      case Just x of
    Nothing ->
        Nothing

    Just value ->
        Just ((\x -> f (g x)) value)

      Definition von Maybe.map

    • = 
      Just ((\x -> f (g x)) x)

      Auswertung des case-Ausdrucks

    • = 
      Just (f (g x))

      Auswertung des lambda-Ausdrucks

Zuletzt betrachten wir noch ein weiteres Beispiel für einen Funktor, um zu illustrieren, dass das Konzept der map-Funktion weit über Container-Datentypen hinausgeht. Zuerst definieren wir das folgende Typsynonym.

type alias Function a b =
    a -> b

Dieser Typ ist ebenfalls ein Funktor und wir können die folgende map-Funktion definieren.

map : (a -> b) -> Function c a -> Function c b
map f g =
    \c -> f (g c)

Es handelt sich bei dieser Funktion um die Definition der Funktionskomposition.

Wir wollen nun einmal zeigen, dass diese Implementierung der Funktion map ebenfalls die beiden Funktorgesetze erfüllt. Seien t1 und t2 Typen und sei fx vom Typ Function t1 t2. Dann gilt das Folgende.

map (\x -> x) fx
  • = 
    \c -> (\x -> x) (fx c)

    Definition von map

  • = 
    \c -> fx c

    Anwendung des Lambda-Ausdrucks

  • = 
    fx

    Eta-Reduktion

Seien t1, t2, t3 und t4 Typen. Seien fx vom Typ Function t1 t2, f vom Typ t3 -> t4 und g vom Typ t2 -> t3. Dann gilt das Folgende.

map f (map g fx)
  • = 
    map f (\c -> g (fx c))

    Definition von map

  • = 
    \d -> f ((\c -> g (fx c)) d))

    Definition von map

  • = 
    \d -> f (g (fx d))

    Anwendung des Lambda-Ausdrucks

  • = 
    \c -> f (g (fx c))

    Umbenennung des Argumentes

  • = 
    map (\x -> f (g x)) fx

    Definition von map