Typen ... mit Sicherheit

Schuld ist dieses Bild

Types

und ich mit meiner großen Klappe:


Natürlich ist am Bild was dran - für die meisten von uns sind Typen schlimsten Falls lästig und besten Falls das, was uns IntelliSense und nette Refaktoring- Tools wie ReSharper schenkt (wenn ich Mike glauben darf - und das tue ich - dann stimmt das so nicht aber darum soll es hier nicht gehen).

Das ist aber nur das eine Ende des Spektrums - sozusagen der Ultaviolette Bereich - heiß her geht es am anderen Ende und darum geht es.

Von Karten und ein paar Farben

Habt ihr schon mal vom 4-Farben Satz gehört?

Einfach gesprochen geht es darum, ob ein kluger Mensch auf jeder beliebigen Landkarte die einzelnen Länder so mit nur 4 unterschiedlichen Farben einfärben kann, dass niemals 2 benachbarte Länder mit der gleichen Farbe ausgemalt werden können:

Beispiel > (Quelle: Wikimedia.org)

Die Variante mit 5 Farben ist nicht einmal so schwer zu beweisen, aber an der Version haben sich Mathematiker und Amateure ziemlich lange die Zähne ausgebissen (so zwischen 1852 bis in die 60er Jahre des letzten Jahrhunderts).

Der Beweis hatte (und hat) aber einen faden Beigeschmack - denn leider ist es zwar gelungen die erstmal ziemlich unendliche Anzahl an unterschiedlichen Karten auf ca. 630 zu reduziern, aber diese wurden und werden mit einem Computerprogramm verifiziert (d.h. der Computer sucht korrekte Färbungen).

Wie jeder von uns weiß ist es ziemilch schwierig (aussichtslos?) wirklich Bugfreie Software zu schreiben - wer also garantiert, dass nicht einer der Fälle wegen eines Bugs im Programm als korrekt markiert wurde?

Genau hier kommen die Typen ins Spiel - 2005 ist es nämlich gelungen einen formalen Beweis in Coq einem sogenannten Proof Assistant zu programmieren d.h. das Programm das die Fälle durchspielt wurde in Coq umgesetzte - für die Obernerds: hier ist das Paper das ich übrigens (noch?!) nicht gelesen habe.

Mathematiker finden das übrigens immer noch unbefriedigend (wer garantiert das der Coq-Typchecker/Compiler richtig arbeitet, oder die Hardware,...)

Typen, Theoreme und Beweise

Ok wo kommen jetzt die Typen rein?

Durch den sogenannten Curry-Howard Isomorphimus - das ist übrigens der Curry, dessen Vorname Haskell ist ;)

Der besagt grob gesprochen, dass man Typen als mathematische Behauptungen (Theoreme) und die Funktionen/Werte/Programme, die diese Typen implementieren als Beweise dieser Behauptung betrachten kann.


Eine schöne Einführung könnt ihr euch übrigens direkt vom Lambda-Man höchst persönlich anschauen (unbedingt machen!):

Philip Wadler - Propositions as Types


Und genau das ist das andere Ende des Spektrums: Typen sind mathematische Wahrheiten - zumindestens dann wenn wir schön pure bleiben und keine allgemeine Rekursion benutzen (hatte ich das nicht bemerkt: Turing vollständigkeit bzw. μ-Rekursion könnt ihr hier vergessen ... ist aber tatsächlich gar nicht sooo wichtig ;) ).

Deshalb hat mich das Bild auch so getriggert.

Ein kleines Beispiel

Aber ihr wollt Code oder?

Na gut - mit JS, C#, F# und Haskell halten wir uns lieber gar nicht erst auf, da können wir mit

endeDerVernunft : a
endeDerVernunft = endeDerVernunft

(auch als undefined oder Bottom bekannt ;) ) alles Beweisen - also auch Unsinn.

Aber Idris ist ganz nett - da können wir den Compiler nämlich fragen, ob unsere Funktionen/Beweise total sind (sollten sie sein).

ist ein Element in der Liste

Gesucht ist ein Programm, dass entscheidet, ob ein Element in einer Liste ist.

Naiv also etwas wie

inListe : a -> List a -> Bool

Leider nützt das nicht viel - die Behauptung hier ist wertlos, wir können nämlich einfach etwas wie

inListe : a -> List a -> Bool
inListe x xs = True

angeben - was korrekt ist, aber nicht ganz dem Sinn entspricht.

Es gilt also den Sinn auszudrücken und das heißt als Typ.

Die Idee ist eigentlich ganz einfach: wir geben über den Typ die Stelle an, wo das Element gefunden werden kann:

data InListe : a -> List a -> Type where
  Hier : InListe x (x :: rest)
  Dort : (InListe x xs) -> InListe x (y :: xs)

Ihr könnt das einfach(sic) so lesen:

Ein Wert x:a ist in einer Liste xs:List a, falls die Liste entweder mit x :: ... angeht (der Hier Fall), oder falls wir wissen, dass der Wert irgendwo in xs vorkommt (InListe x xs) und die Liste die Form y :: xs für irgendein y:a hat.

Willkommen in der Welt des Wahnsinns - a.k.a. Dependent Types!

Die Funktion selbst sieht dann so aus:

istInListe : DecEq a => (x:a) -> (xs:List a) -> Dec (InListe x xs)
istInListe x [] = No nichtsIstInLeererListe
istInListe x (y :: xs) with (decEq x y)
  istInListe x (x :: xs) | (Yes Refl) = Yes Hier
  istInListe x (y :: xs) | (No nichtHier) = 
    case istInListe x xs of
      Yes dort => Yes (Dort dort)
      No nichtDort => No (nichtHierNichtDortNirgends nichtHier nichtDort)

Ich kann an der Stelle nicht auf alle Details eingehen (falls Ihr interesse habt mache ich gerne eine Serie daraus - schreibt mich an!), aber im Prinzip steht da das:

istInListe x [] = No nichtsIstInLeererListe

in der leeren Liste ist gar nichts

istInListe x (y :: xs) with (decEq x y)

um zu entscheiden, ob x in y :: xs ist, schau doch erstmal ob x gleich y ist

istInListe x (x :: xs) | (Yes Refl) = Yes Hier

falls ja (man beachte: jetzt weiß Idris, das x und y dasselbe sind und wir dürfen x (x :: xs) schreiben haben wir einen Beweis Hier gefunden ... also Ja x ist genau hier

istInListe x (y :: xs) | (No nichtHier) = 
    case istInListe x xs of

falls x nicht gleich y war, schau doch, ob x in xs vorkommt (zurück kommt ein Beweis oder ein Gegenbeweis!)

Yes dort => Yes (Dort dort)

Hey ja x kommt dort vor - also entsprechenden Beweis zurück.

No nichtDort => No (nichtHierNichtDortNirgends nichtHier nichtDort)

Nein? ... Mist, wenn er nicht hier war und auch nicht dort dann kommt der Wert also nicht vor - das Lemma beweist das dann noch auf Typebene.

Hilfslemmas

wobei die beiden Hilf-Lemmas

nichtsIstInLeererListe : InListe x [] -> Void
nichtsIstInLeererListe Hier impossible
nichtsIstInLeererListe (Dort _) impossible

nichtHierNichtDortNirgends : (nichtHier : (x = y) -> Void) -> (nichtDort : InListe x xs -> Void) -> (contra: InListe x (y :: xs)) -> Void
nichtHierNichtDortNirgends nichtHier nichtDort Hier = nichtHier Refl
nichtHierNichtDortNirgends nichtHier nichtDort (Dort dort) = nichtDort dort

benutzt wurden.

Was hab ich jetzt davon? Naja - diese Implementation kann eigentlich nicht falsch sein, wenn die schlauen Leute mit Idris keinen Fehler gemacht haben.

Ich kann nicht bescheißen und bekomme mit Sicherheit (Beweis) zurück ob der Wert drin liegt (und wo) oder nicht.

Das kann ich dann zum Beispie verwenden um Typsichere remove, etc. zu schreiben.


Fazit

Will ich das überall machen?

Wahrscheinlich nich - aber es geht und wenn ihr das richtige Typsystem wählt könnt ihr euch irgendwo zwischen es nervt = Bild und ihr programmiert nicht sonder macht Mathe = Idris/Agda/Coq/... bewegen - ich würde F#, Haskell und co. empfehlen ;)