© Roman Stetsyk / 123RF.com

Haskell entwickelt dank einiger origineller Konzepte auf einer soliden, mathematischen Grundlage ganz besondere Stärken. So kann es etwa eigene Datentypen für Matrizen definieren, die von sich aus viele Voraussetzungen prüfen, was in anderen Sprachen eigene Funktionen übernehmen müssten.

Haskell gibt es schon ziemlich lange, genauer gesagt seit Ende der 1980er-Jahre. Die universitäre Forschung hatte sich zu dieser Zeit schon länger mit funktionaler Programmierung als zukunftsweisendem Paradigma beschäftigt. Standard ML, CAML, Miranda, Hope und Scheme waren damals prominente funktionale Sprachen. In den zu dieser Zeit noch winzigen Communities zeichneten sich schon klare Demarkationslinien ab:

• statische Typsysteme vs. dynamische Typen.
• strikte vs. nicht strikte Auswertung.

Die Unterscheidung zwischen statischen und dynamischen Typen existiert in der heutigen Landschaft immer noch, zwischen Sprachen wie Python, Ruby oder Lua (dynamische Typen) auf der einen und Java sowie Rust (statische Typen) auf der anderen Seite. Die heutigen statischen Typsysteme sind fast alle Abkömmlinge der bahnbrechenden Arbeit aus der funktionalen Programmierung damals. Was wir heute als Generics kennen, nahm in Standard ML seinen Anfang.

Das zweite Unterscheidungsmerkmal, strikt vs. nicht strikt, ist dagegen den meisten heutigen Programmiersprachen fremd. Dabei geht es um Aufrufe von Funktionen beziehungsweise Methoden, die Argumente übergeben. Wird etwa im Term »f(g(x))« zunächst »g(x)« ausgewertet und dann »f()« aufgerufen? Fast alle gängigen Programmiersprachen beantworten diese Frage heute mit ja. Damals allerdings gab es einige wenige Sprachen – Hope und Miranda – die nicht strikt waren, also den Aufruf von »g(x)« erst auswerteten, wenn das Ergebnis tatsächlich benötigt wurde.

Das klingt merkwürdig. In erster Näherung führt es dazu, dass »g(x)« gar nicht ausgewertet wird, wenn »f()« es nicht benötigt. Nun benutzt das durchschnittliche Programm in einer strikten Sprache alle Argumente eines Funktionsaufrufs. In nicht strikten Sprachen schreibt man aber andere Programme. Zum Beispiel kann ein nicht striktes Programm scheinbar unendliche Datenstrukturen bauen. Sie werden nur so weit ausgewertet, wie das Programm ihren Inhalt anfragt. Die nicht strikte Auswertung erlaubt so, fast alle Kontrollstrukturen konventioneller Sprachen in die Daten zu verlegen und damit sehr flexible Modularität herzustellen.

Die Forschung bei nicht strikten Sprachen konzentrierte sich damals auf Miranda, wurde aber jäh gebremst, als der Miranda-Erfinder die Sprache zu kommerzialisieren versuchte und Schutzrechte anmeldete. Im Zorn wendete sich 1987 eine Gruppe von Forschern von Miranda ab, um eine neue nicht strikte Programmiersprache mit statischen Typen zu entwickeln. Kurz darauf war Haskell geboren, und das Interesse an Miranda versiegte schlagartig. Kurioserweise wurde Miranda übrigens im Jahr 2020 endlich doch Open Source.

Haskell ist also älter als Java. Wer aber von Java zu Haskell wechselt, reibt sich die Augen: Die Sprache sieht aus wie von hyperfortschrittlichen Aliens über der Erde abgeworfen, mit grundsätzlich anderen Konzepten zu Syntax und Programmierung. Das liegt daran, dass sich um Haskell seit den Anfängen eine äußerst umtriebige Forschergemeinde kümmert, die immerzu publizieren muss und sich dafür neue Features ausdenkt.

Nun könnte man meinen, dass die Sprache deswegen unter der schieren Last der Features kompliziert und irgendwie zusammengebastelt erscheint, tatsächlich ist alles aber sehr durchdacht und steht auf soliden Grundlagen, die schon in den 1980er-Jahren gelegt wurden. Der Ausführungskern basiert auf dem Lambda-Kalkül, also einer mathematischen und damit äußerst stabilen Grundlage. Er nutzt ein statisches Typsystem auf der Basis von Standard ML (ebenfalls eine solide mathematische Grundlage), das um sogenannte Typklassen erweitert wurde.

Die Innovationen bei Haskell beschränken sich nicht auf die Sprache, sondern beziehen auch den Compiler ein: Der kontinuierlich weiterentwickelte Glasgow Haskell Compiler (GHC) feiert dieses Jahr seinen 30. Geburtstag. Die Entwicklung begann zwar an der Universität Glasgow, ist aber inzwischen weltweit verteilt und wird bei Microsoft Research koordiniert. Der Compiler kann ziemlich gut optimieren. Das muss er auch, um die Ineffizienzen der nicht strikten Auswertung zu kompensieren. Außerdem bietet er erstklassige Unterstützung für nebenläufige und parallele Programmierung.

Neben dem GHC gab es früher noch eine Reihe anderer Haskell-Implementierungen, die aber alle über die Jahre ausstarben; die Entwicklungsanstrengungen konzentrierten sich nach und nach auf den GHC. Neue Sprachfeatures schlagen entsprechend zunächst im GHC auf und sind dort effektiv für alle Haskell-Entwickler verfügbar.

Da es Einführungen in Haskell inzwischen zuhauf gibt, konzentriert sich dieser Artikel auf einige speziellere Features, die unter der Überschrift Dependent Types firmieren. Es geht um die Programmierung auf Typebene. Wir zeigen das anhand des Umgangs mit Array- beziehungsweise Vektordimensionen: Das kann Haskell im Gegensatz zu fast allen anderen gängigen Sprachen auf der Typebene abbilden. Das wiederum erlaubt dem Compiler, besonders häufige Fehler beim Umgang mit solchen Typen zu finden.

Dieses etwas spezielle, aber hoffentlich instruktive Beispiel soll nicht darüber hinwegtäuschen, dass Haskell noch viel mehr kann und sich für Softwareprojekte fast aller Art eignet. Es kann aber hoffentlich einen kleinen Einblick in die Sprache geben, der neugierig auf mehr macht.

Eine Matrix typen

Der Umgang mit linearer Algebra hat mit dem phänomenalen Aufschwung des Deep Learning wieder an Bedeutung gewonnen. Da werden jede Menge Matrizen multipliziert. Wer das schon einmal von Hand gemacht hat, der weiß, dass dabei die Dimensionen der Matrizen zueinander passen müssen.

Die Formel aus Abbildung 1 berechnet das Produkt »C=AB« zweier Matrizen »A« und »B«, wobei man die Elemente von »A« als »a_ij« bezeichnet. »i« steht hier für die Zeile, »j« für die Spalte. Entsprechend handelt es sich bei »b_jk« um die Elemente von »B« und bei »c_ik« um jene von »C«. Das funktioniert nur, wenn »A« ebenso viele Spalten hat wie »B« Zeilen; in der Formel ist das mit »n« bezeichnet.

Abbildung 1: Diese Formel berechnet das Produkt »C=AB« zweier Matrizen »A« und »B«.

Sehen wir uns zunächst einmal an, wie man das in einer gängigen Sprache wie Java realisiert. Zunächst einmal gilt es, eine geeignete Repräsentation zu wählen – in Java sind Arrays genau dafür gemacht. Das Array »A« sieht dann in Java so aus:

double[][] a;

Für diese Repräsentation lässt sich eine statische Methode für die Matrixmultiplikation so schreiben wie in Listing 1. Bei den Parametern »m«, »n« und »p« handelt es sich um die Dimensionen. »A« ist eine »m*n«-Matrix, »B« eine »n*p«-Matrix und »C« eine »m*p«-Matrix.

public static double[][] multiply(int m, int n, int p, double[][] a, double[][] b) {
  double[][] c = new double [m][p];
  for (int i = 0; i < m; ++i) {
    for (int j = 0; j < p; ++j) {
      c[i][j] = 0;
      for (int k = 0; k < n; ++k) {
        c[i][j] += a[i][k] * b[k][j];
      }
    }
    return c;
  }
}

Dabei gibt es allerdings ein kleines Problem: Die Dimensionen sind nicht Teil des Typs und werden erst bei der Konstruktion angegeben. Es sind also alle Matrix-Typen gleich, und der Compiler kann nicht überprüfen, ob die Dimensionen der multiplizierten Matrizen überhaupt zueinander passen. Man könnte sich aber ein Paralleluniversum vorstellen, in dem Java erlaubt, die Dimensionen als Teil der Typen hinzuschreiben. Dann sähe die Signatur von »multiply()« so aus wie in Listing 2.

public static double[m][p] multiply(int m, int n, int p, double a[m][n], double b[n][p])

Das brächte präzise den Zusammenhang der Dimensionen von »a«, »b« und »c« zum Ausdruck (Abbildung 2). So unscheinbar das aussieht, erfordert es ein vollkommen neues Konzept im Java-Typsystem: »m«, »n« und »p« sind Werte, und die Typen von »a« und »b« (und des Ergebnisses) hängen von diesen Werten ab. Dieses Phänomen heißt auf Englisch Dependent Types, und die gibt es in Java nicht.

Abbildung 2: Dieses Schema verdeutlicht die Abhängigkeiten zwischen Werten und Typen.

Haskell-Basics

Wir beschränken uns in diesem Artikel nur auf jene Features von Haskell, die für die Programmierung von Matrizen mit Dependent Types unbedingt notwendig sind. Hier ist eine Datentypdefinition für sogenannte natürliche Zahlen, also die Zahlen 0, 1, 2 und so weiter:

data Nat = Zero | Succ Nat

Der senkrechte Strich »|« steht für “oder” und trennt die Fälle einer Datentypdefinition. Damit bedeutet der Ausdruck so viel wie: Eine natürliche Zahl ist die Null oder der Nachfolger einer natürlichen Zahl. Nachfolger ist ein anderes Wort für +1. In einer objektorientierten Sprache würde man eine kleine Klassenhierarchie bauen, mit einem Interface »Nat« und zwei Klassen »Zero« und »Succ«, die es implementieren.

Es handelt sich um eine Definition aus der Mathematik – typisch für die funktionale Programmierung. Freilich sind Zahlen in Haskell auch eingebaut, aber wir werden diese selbst gebastelte Definition noch für die Matrixmultiplikation benötigen.

Diese Datentyp-Definition können wir nun benutzen, um ein paar Definitionen für Werte in Form von Gleichungen hinzuschreiben (Listing 3, Zeile 1 bis 4). Das wirkt recht umständlich, aber man sieht, wie die Zahlen zustande kommen. Zu einer Gleichung lässt sich in Haskell auch immer eine Typsignatur angeben (Zeile 5 bis 8).

zero = Zero
one  = Succ Zero
two = Succ one
three = Succ two
zero :: Nat
one  :: Nat
two  :: Nat
three :: Nat

Da die Zahlen in »Nat« selbst gebastelt sind, müssen wir auch die Operationen darauf selbst schreiben. Listing 4 zeigt als Beispiel die Addition. Die drei Zeilen definieren eine Funktion namens »add«. Die erste Zeile legt die Typsignatur fest, die besagt, dass »add« zwei »Nat«-Instanzen als Eingaben und eine als Ausgabe verwendet.

add :: Nat -> Nat -> Nat
add Zero n = n
add (Succ m') n = Succ (add m' n)

Die beiden nächsten Zeilen enthalten Gleichungen, und zwar eine pro Fall der Datentypdefinition für »Nat«. Die erste Gleichung ist für »Zero« zuständig. Dort steht sinngemäß, dass die Summe aus »Zero« und einer Zahl »n« gleich »n« ist. Die zweite Gleichung drückt aus, dass die Summe aus dem Nachfolger einer Zahl »m’« (“M-Strich”) und einer Zahl »n« der Nachfolger der Summe von »m’« und »n« ist.

Der Mechanismus, der es erlaubt, Funktionen auf so kompakte Art und Weise zu definieren, heißt Pattern Matching. Die Gleichungen zeigen, dass Funktionsaufrufe in Haskell ohne Klammern auskommen: Man schreibt einfach die Funktion und die Argumente hintereinander. Zum Beispiel liefert »add two three« das Ergebnis »Succ (Succ (Succ (Succ (Succ Zero))))«, also »5«.

Listen

Zu den spannenderen Features von Haskell gehört der Umgang mit Listen. Die sind in der Sprache fest eingebaut, aber wir definieren sie zu Demonstrationszwecken in Listing 5 selbst. Dabei kommen gleich zwei neue Features ins Spiel. Zunächst bekommt der Typ »List« einen Typparameter namens »a«. Das entspricht einem Generic in Java.

data List a = Nil | a :> List a
infixr 5 :>

Außerdem wird der zweite Konstruktor als Infix-Operator definiert, den man wie »+« und »*« dazwischen schreibt. Die »infixr«-Zeile besagt, dass der Operator von rechts geklammert wird, und bezeichnet außerdem dessen Präzedenz – also wie genau er in die Hierarchie der Punkt-vor-Strich-Rechnung passt. Die Listenelemente hängt man also mit »:>« aneinander; »Nil« terminiert das Konstrukt.

Die Datendefinition bedeutet insgesamt: Eine Liste aus »a«-Elementen ist entweder »Nil« (also eine leere Liste) oder eine nicht leere Liste (auch »Cons«-Liste genannt) aus einem Element »a« und einer Liste von »a«-Elementen. Listing 6 zeigt einige Beispiele dafür.

list1, list2 :: List Double
list1 = 1 :> 2 :> 3 :> Nil
list2 = 3 :> 4 :> 5 :> Nil
list3, list4, list5 :: List Double
list3 = 7 :> 8 :> Nil
list4 = 9 :> 10 :> Nil
list5 = 11 :> 12 :> Nil

Listing 7 demonstriert eine einfache Funktion auf solchen Listen. Der Aufruf »sum list1« ergibt zum Beispiel »6«. Bei der ersten Zeile handelt es sich wieder um eine Typsignatur (Liste von »Double«-Zahlen rein, »Double« raus). Die erste Gleichung besagt schlicht, dass die Summe der leeren Liste gleich null ist. Die zweite definiert die Summe einer Cons-Liste mit dem ersten Element »x« und dem Rest »xs« als »x« plus die Summe von »xs«.

sum :: List Double -> Double
sum Nil = 0
sum (x :> xs) = x + (sum xs)

Das Beispiel zeigt, dass man »List« in Typsignaturen nicht allein verwenden kann – es gilt stets, den Typ der Elemente mit anzugeben. Das macht »List« zu einem Typkonstruktor, also so etwas wie einer Funktion auf Typebene: Der Typ der Elemente geht hinein, heraus kommt der Typ der Listen mit diesem Elementtyp. Mit anderen Worten: Auch »List« hat so etwas wie einen Typ, der sich in Haskell folgendermaßen schreibt:

type List :: Type -> Type

Das sieht also aus wie die Signatur für eine Funktion, nur eben mit dem Wörtchen »type« am Anfang. Solche Typen der Typen heißen in Haskell Kind (engl. für Art), und um sie zu benutzen, schaltet man über eine magische Zeile (Listing 8, erste Zeile) am Anfang der Quelldatei ein spezielles Feature in GHC ein. Der Kind namens »Type« muss man außerdem aus einer Library importieren (zweite Zeile).

{-# LANGUAGE StandaloneKindSignatures #-}
import Data.Kind (Type)

Schreiben wir noch ein paar weitere Funktionen auf Listen. Listing 9 implementiert die bekannte »map«-Funktion, die eine beliebige Funktion auf alle Elemente einer Liste anwendet und eine Ergebnisliste liefert.

map :: (a -> b) -> List a -> List b
map f Nil = Nil
map f (x :> xs) = (f x) :> (map f xs)

Auch hier spielen Typvariablen eine wichtige Rolle: Die Typsignatur bedeutet: Übergibt man »map« eine Funktion, die aus einem »a« ein »b« macht, sowie eine Liste von »a«-Elementen, liefert es eine Liste von »b«-Elementen. Die Gleichungen funktionieren nach demselben Muster wie bei »sum«. Die »map«-Funktion ließe sich zum Beispiel so aufrufen:

map (\ x -> x * 2) list1

Der Backslash »\« steht für Lambda. Man muss das Alter von Haskell berücksichtigen, um das zu verstehen: In den 1980-ern gab es noch kein Unicode, und so verwendete man das ASCII-Zeichen, das dem griechischen Lambda am ähnlichsten sieht. Der Ausdruck innerhalb der Klammern definiert eine Funktion mit dem Parameter »x«, die das Argument mit 2 multipliziert. Dementsprechend kommt dabei folgende Liste heraus:

2 :> 4 :> 6 :> Nil

Die »map«-Funktion operiert nur auf einer Liste. Manchmal gilt es, zwei Listen zu kombinieren – zum Beispiel für die Matrixmultiplikation. Dafür gibt es die Funktion »zipWith« (Listing 10). Deren Typsignatur besagt: Gegeben sei eine Funktion, die aus einem »a« und einem »b« ein »c« macht, sowie je eine Liste aus »a«- und »b«-Elementen. Dann liefert »zipWith« eine Liste aus »c«-Elementen.

zipWith :: (a -> b -> c) -> List a -> List b -> List c
zipWith f Nil Nil = Nil
zipWith f (x :> xs) (y :> ys) = (f x y) :> (zipWith f xs ys)

Der Funktionsname bezieht sich auf das Reißverschlussverfahren, nach dem der Code vorgeht (Abbildung 3). Die zweite Zeile in Listing 8 besagt, dass zwei leere Listen kombiniert wieder eine leere Liste ergeben. Die zweite Gleichung drückt aus, dass man beim Kombinieren zweier nicht leerer Listen die ersten Elemente mit »f« kombiniert und dann davor die Kombination der beiden Restlisten hängt. Hier ein Beispielaufruf für »zipWith«:

zipWith (*) list1 list2

Abbildung 3: Das Reißverschlussverfahren in der Funktion »zipWith«.

Hier werden die beiden Listen elementweise multipliziert. Das »*« muss in Klammern, weil Haskell es sonst für einen Infix-Operator hält. Heraus kommt Folgendes:

3 :> (8 :> (15 :> Nil))

Die Funktion »zipWith« erweist sich insofern als problematisch, als sie erwartet, dass beide Eingabelisten dieselbe Länge haben, ohne dass das in der Typsignatur steht und dass der Compiler es prüfen könnte. Ist diese Bedingung nicht erfüllt, gibt es eine Fehlermeldung zur Laufzeit (Listing 11).

> zipWith (*) list1 Nil
*** Exception: Non-exhaustive patterns in function zipWith

Jetzt können wir einen ersten Versuch unternehmen, einen Typ für Matrizen mithilfe von Listen zu definieren, analog zur Array-Repräsentation in Java. Gemäß der Definition aus der ersten Zeile von Listing 12 handelt es sich bei einer Matrix einfach um eine Liste von Listen. Die zweite Zeile erzeugt eine Matrix mit zwei Zeilen aus jeweils drei Spalten.

type Matrix a = List (List a)
matrix1 = list1 :> list2 :> Nil

Die Matrix-Multiplikation lässt sich am einfachsten mithilfe einer Transposition schreiben, also einer Funktion, die eine Matrix um 90 Grad dreht beziehungsweise Zeilen und Spalten vertauscht. Das lässt sich mithilfe von »zipWith« erledigen.

Die erste Gleichung aus Listing 13 macht aus einer »1*n«-Matrix eine »n«-reihige Matrix, bei der jede Zeile nur eine Spalte hat. Die zweite Gleichung teilt die Matrix in die erste Zeile und den Rest auf. Der Rest wird transponiert; nun gilt es nur noch, die Spalten der ersten Zeile auf die entstandenen Zeilen zu verteilen. Das erledigt »zipWith«.

transpose :: Matrix a -> Matrix a
transpose (x :> Nil) = map (\ a -> a :> Nil) x
transpose (x :> xs) = zipWith (:>) x (transpose xs)

Dabei fällt auf, dass es keine Gleichung für »Nil« gibt. Das Problem: Die Funktion muss ja die Spaltenanzahl der Eingabematrix kennen. Hat diese aber keine Zeile, dann ist die Anzahl der Spalten unbekannt. Nun endlich können wir »multiply« definieren. Die Funktion aus dem inneren »map« in Listing 14 entspricht der Summe aus der Formel, die eine Zeile aus »a« (»arow«) elementweise mit einer Spalte aus »b« (»bcolumn«) multipliziert und die Produkte aufsummiert.

multiply :: Matrix Double -> Matrix Double -> Matrix Double
multiply a b =
  map (\ arow -> (
        map (\ bcolumn
 -> sum (zipWith (*) arow bcolumn))
        (transpose b)
        )
      )
      a

Neue Dimensionen

Unsere »Matrix« hat allerdings dasselbe Problem wie die Java-Version: Die Dimensionen sind nicht Teil des Typs, und daher kann der Compiler auch nicht prüfen, ob sie zum Beispiel bei »multiply« passen. Wir fangen also noch einmal von vorn an und schalten dafür eine ganze Batterie von GHC-Spracherweiterungen ein (Listing 15).

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}

Statt des Typs »List« definieren wir einen neuen Typ namens »Vec«, der das Problem lösen soll (Listing 16). Er hat also dieselben Fälle wie »List«, wird aber etwas anders definiert: Nach dem »data« steht kein Gleichheitszeichen, sondern ein »where«. Diese Syntax bewirkt, dass für den Konstruktor eines jeden Falls eine Typsignatur angegeben wird. (Bei der Syntax mit Gleichheitszeichen wären es Typen für die Attribute.)

data Vec n a where
  Nil  :: Vec Zero a
  (:>) :: a -> Vec n a -> Vec (Succ n) a

An dieser Stelle kommt der neue Typparameter »n« ins Spiel, der die Länge angibt. Dazu verwendet er den bereits definierten »Nat«-Typ. Die beiden Typsignaturen aus Listing 16 bedeuten:

• »Nil« ist ein Vektor der Länge 0.
• »:>« macht aus einem Element und einem Vektor der Länge »n« einen Vektor der Länge »n+1«.

Wie bei »List« können wir auch für »Vec« einen Kind angeben, der folgendermaßen aussieht:

type Vec :: Nat -> Type -> Type

Er zeigt deutlich, dass »Vec« ein Dependent Type ist, der als erstes Argument Werte vom Typ »Nat« hat. Wir können Vektoren genauso erzeugen wie Listen (Listing 17, erste zwei Zeilen). Allerdings sehen die Typen anders aus: Das »(Succ (Succ (Succ Zero)))« in der letzten Zeile ist ein anderes Wort für »3«, also die Länge der Vektoren. Die Listen-Funktionen aus dem vorigen Abschnitt können wir ganz ähnlich definieren (Listing 18).

vec1 = 1 :> 2 :> 3 :> Nil
vec2 = 3 :> 4 :> 5 :> Nil
vec1, vec2 :: Vec (Succ (Succ (Succ Zero))) Double

sum :: Vec n Double -> Double
sum Nil = 0
sum (x :> xs) = x + (sum xs)
map :: (a -> b) -> Vec n a -> Vec n b
map f Nil = Nil
map f (x :> xs) = (f x) :> (map f xs)
zipWith :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWith f Nil Nil = Nil
zipWith f (x :> xs) (y :> ys) = (f x y) :> (zipWith f xs ys)

Die Gleichungen sind also identisch mit denen aus der »List«-Implementation, aber die Typsignaturen sind aussagekräftiger geworden. Die von »map« besagt, dass die Länge des Ausgabevektors dieselbe ist wie die des Eingabevektors, und die von »zipWith«, dass die beiden Eingabevektoren die gleiche Länge haben müssen. Ist das nicht der Fall, meldet der Compiler einen Typfehler (Listing 19). Das geht schon einmal in die richtige Richtung.

> zipWith (*) vec1 Nil
error:
  * Couldn't match type 'Zero' with 'Succ (Succ (Succ Zero))'
    Expected type: Vec (Succ (Succ (Succ Zero))) Double
      Actual type: Vec Zero Double
  * In the third argument of 'zipWith', namely 'Nil'
    In the expression: zipWith (*) vec1 Nil
    In an equation for 'it': it = zipWith (*) vec1 Nil

Als nächstes kommt »transpose« an die Reihe. Naheliegend wäre es, die Gleichungen unverändert zu übernehmen und nur die Typsignatur aufzubohren (Listing 20). Das funktioniert auch direkt. Allerdings warnt der Haskell-Compiler nun, dass die Funktion beim Pattern Matching nicht alle Fälle des Datentyps abdeckt (Listing 21).

transpose :: Matrix m n a -> Matrix n m a
transpose (x :> Nil) = map (\ b -> b :> Nil) x
transpose (x :> xs) = zipWith (:>) x (transpose xs)

warning:
  Pattern match(es) are non-exhaustive
  In an equation for 'transpose': Patterns not matched: Nil

Das war auch bei der Listenversion schon so, die nicht mit einer leeren Matrix (genauer: einer Matrix mit null Zeilen) umgehen konnte. Das kann hier wie dort zu Laufzeitfehlern führen. Es wäre gut, wenn der Compiler auch dieses Problem erkennen könnte. Dazu müssten wir ausdrücken, dass »m« größer als null ist.

Übertragen auf unseren Datentyp »Nat« bedeutet das, dass »m« die Form »Succ m’« haben muss. Genau das lässt sich in der Typsignatur durch einen sogenannten Constraint ausdrücken (Listing 22). Damit verschwindet zwar die Warnung aus Listing 21, dafür wirft der Compiler nun eine recht heftige Fehlermeldung (Listing 23). Sie besagt, dass es ein Problem mit der zweiten Gleichung gibt, weil der Typ »m’« nicht die Form »Succ m’0« hat. Warum?

transpose :: (m ~ Succ m') => Matrix m n a -> Matrix n m a

error:
  * Couldn't match type 'm'' with 'Succ m'0'
      arising from a use of 'transpose'
    'm'' is a rigid type variable bound by
      the type signature for:
        transpose :: forall (m :: Nat) (m' :: Nat) (n :: Nat) a.
                     (m ~ Succ m') =>
                     Matrix m n a -> Matrix n m a
  * In the third argument of 'zipWith', namely '(transpose xs)'
    In the expression: zipWith (:>) x (transpose xs)
    In an equation for 'transpose':
        transpose (x :> xs) = zipWith (:>) x (transpose xs)

Bei »m’« handelt es sich um den Typ des Rests der Matrix, also den Typ von »xs«. Der Compiler besteht darauf, dass »m’« größer als null sein muss – das ist die Voraussetzung für den rekursiven Aufruf von »transpose« mit »xs«. Das könnte man zwar aus den Gleichungen herauslesen, der Compiler schafft das aber nicht.

Wir müssen die zweite Gleichung etwas expliziter machen. Sie sieht dann so aus wie in Listing 24. Das Anhängsel »@(y :> ys)« besagt, dass »xs« die Form »(y :> ys)« haben muss, also eine nicht leere Liste ist. Das genügt GHC, und er akzeptiert die Definition. Schließlich fehlt noch »multiply«, das wieder funktioniert wie gehabt (Listing 25).

transpose (x :> xs@(y :> ys)) = zipWith (:>) x (transpose xs)

multiply :: (n ~ Succ n')  => Matrix m n Double -> Matrix n p Double -> Matrix m p Double
multiply a b =
  map (\ ar -> (map (\ bc -> sum (zipWith (*) ar bc)) (transpose b))) a

Man sieht dem Typ also nun genau an, wie die Dimensionen der Matrizen zusammenpassen – so war das Ganze gedacht.

Fazit

Dependent Types machen Haskells Typsystem extrem mächtig: Es vermag Dinge auszudrücken, die in den meisten anderen Sprachen undenkbar sind. Das hat zwei positive Konsequenzen: Die Typsignaturen lesen sich für den Menschen sehr aussagekräftig, und der Compiler kann viele Fehler finden, die in schwächeren Typsystemen unentdeckt bleiben. Damit wirft Haskells Typsystem ein Schlaglicht auf eine Entwicklung bei Programmiersprachen, die uns in den nächsten Jahren begleiten wird und muss, weil die Anforderungen an Korrektheit und Zuverlässigkeit steigen. (jcb/jlu)