Im vorherigen Artikel dieser Reihe warfen wir einen Blick auf die Programmiersprache Agda. Mit Agda kann man komplexe Spezifikationen ausdrücken und beweisen, dass der Code, den man gegen diese Spezifikationen schreibt, diese auch einhält. Wir hatten das anhand der natürlichen Zahlen und des Zusammenhangs von der Unärdarstellung und der Binärdarstellung illustriert. Zur Erinnerung: Wir hatten die unären natürlichen Zahlen so als Daten beschrieben:
data Nat : Set where
zero : Nat
suc : Nat -> Nat
Und die Binärdarstellung so:
data Bin : Set where
0b : Bin
1b : Bin
at-0 : Bin -> Bin
at-1 : Bin -> Bin
Um diese zwei Darstellungen ins korrekte Verhältnis zu setzen, hatten wir eine explizite Semantikfunktion geschrieben:
μ : Bin -> Nat
μ 0b = zero
μ 1b = one
μ (at-0 x) = (* two (μ x))
μ (at-1 x) = (+ (* two (μ x)) one)
Wir hatten dann noch eine einfache Funktion auf den binären Zahlen definiert:
inc : Bin -> Bin
inc 0b = 1b
inc 1b = 10b
inc (at-0 x) = at-1 x
inc (at-1 x) = at-0 (inc x)
Unser Korrektheitskriterium von inc und der entsprechende Beweis war
dann eine weitere Funktion:
inc===+1 : (x : Bin) -> === (μ (inc x)) (+ (μ x) one)
inc===+1 = ...
Das ist alles ganz ok. Schöner wäre es allerdings, wenn Funktion und
Korrektheit näher beieinander wären. Schließlich ist der Reiz an
statisch typisierten Programmiersprachen, dass der Doppelpunkt nicht
nur Werte mit deren Typen ins Verhältnis setzt (was soll das überhaupt
bedeuten?), sondern gleichzeitig Implementierungen zu deren
Interfaces. In vielen Programmiersprachen ist die Sprache der
Interfaces sehr beschränkt. In Agda können wir fast jede mathematische
Aussage als Typ – also als Interface – formalisieren. Das haben wir
bei der Funktion inc oben allerdings versäumt. Deren Typ
bzw. Interface ist lediglich Bin -> Bin, was ja nun fast alles
bedeuten kann. Bekommen wir die ganze Semantik der inc-Funktion in
ihre Typsignatur gepackt? Das hätte offensichtliche Vorteile für den
Verwender, aber auch wir als Implementierer hätten die Sicherheit,
dass jede Implementierung von inc, die typcheckt, auch eine
korrekte Implementierung wäre.
Ein neuer Versuch
Die Definition der unären natürlichen Zahlen behalten wir einfach bei. Auch die Addition und Multiplikation auf den Unärzahlen werden weiterhin nützlich sein.
Die Binärzahlen definieren wir jetzt allerdings direkt mit Verweis auf die Unärzahlen. Dafür statten wir den Typen der Binärzahlen mit einem Typindex aus:
one : Nat
one = suc zero
two : Nat
two = suc one
-- .----- hier ist der Typindex
-- |
-- v
data Bin : Nat -> Set where
0b : Bin zero
1b : Bin one
_-0b : {n : Nat} -> Bin n -> Bin (* n two)
_-1b : {n : Nat} -> Bin n -> Bin (+ one (* n two))
Typindizes hatten wir bereits im letzten Artikel kennen gelernt. Der
erste Fall beschreibt, dass die Binärzahl (streng genommen: der
Binärzahlkonstruktor) 0b nicht einfach vom Typen Bin ist, sondern
vom Typen Bin zero. Die entsprechende Unärzahl steckt also im
Typen der Binärzahl. Bei 1b ist der Typ dann auch nicht Bin und
auch nicht Bin zero, sondern Bin (suc zero).
Die zwei nächsten Typkostruktoren sind etwas anspruchsvoller. Wir
haben uns hier zunächst erlaubt, zwei Postfix-Konstruktoren zu
definieren. Mit dem Unterstrich am Anfang geben wir an, dass das eine
Argument für diese Konstrutoren vor dem Operator -0b bzw. vor dem
Operator -1b stehen muss. Damit können wir unsere Binärzahlen in
einer Notation verfassen, die der üblichen Schreibweise näher
kommt. Die „Sechs“ (binär: 110) wäre bei uns 1b -1b -0b. Semantisch
bedeutet die Typsignatur von -0b, dass wir eine natürliche Zahl
brauchen ({n : Nat}) und dann aus einer Binärzahl vom Typen Bin n
eine Binärzahl vom Typen Bin (* n two) zu machen. Da wir n : Nat
in geschweiften Klammern geschrieben haben, handelt es sich dabei um
einen impliziten Parameter. Implizite Parameter darf man beim Aufruf
oft weg lassen. Agda füllt den Parameter dann intern automatisch. Hier
lässt sich beispielsweise das implizite n aus dem Typen des nächsten
Parameters Bin n erschließen.
Der Konstruktor -1b funktioniert ähnlich. Auch hier haben wir einen
impliziten Parameter n : Nat und eine Binärzahl Bin n. Raus kommt
eine Binärzahl Bin (+ one (* n two)). Die vier Fälle in dieser
Datentypdefinition entsprechen exakt der Definition unserer
Semantikfunktion μ. Die Semantik der Binärzahlen ist diesen jetzt
also in Form ihrer Typen eingeschrieben. Wir brauchen die externe
Funktion μ gar nicht mehr – auch nicht für die Beschreibung der
Korrektheit einer Inkrementierfunktion:
inc : {n : Nat} -> Bin n -> Bin (suc n)
inc = ?
Die Typsignatur von inc drückt hier bereits ihre ganze gewünschte
Semantik aus. inc soll eine Funktion sein, die die Binärdarstellung
einer Zahl n auf die Binärdarstellung einer Zahl (suc n)
abbildet. Der implizite Parameter {n : Nat} stört vielleicht noch
ein wenig. Mit etwas Refactoring bekommen wir den aber zumindest an
eine andere Stelle verfrachtet. Wir definieren uns eine Funktion, die
den Typen beschreibt, der besagt, dass wir eine gegebene einstellige
Funktion auf den Unärzahlen in die Welt der Binärdarstellungen heben
wollen.
binop : (Nat -> Nat) -> Set
binop f = {n : Nat} -> Bin n -> Bin (f n)
Die Implementierung für inc ist die, die wir schon kennen:
inc : binop suc
inc 0b = 1b
inc 1b = 1b -0b
inc (x -0b) = x -1b
inc (x -1b) = inc x -0b
Das checkt Typ und ist damit korrekt. Ein Verwender kann sich jetzt
allein anhand der Typsignatur binop suc sicher sein, dass inc das
Hochzählen auf Binärzahlen implementiert.