Abhängige und Verfeinerungsarten: Warum?

Dieser Artikel wurde ursprünglich auf 47deg.com am 14. September 2020 veröffentlicht.

Da sind wir wieder. Als Sie dachten, dass Summe und Produkt, im Wesentlichen algebraische Datentypen, der letzte Schritt auf der Leiter sind, tauchen neue Namen auf. Aber warum sind wir so versessen auf (starke) Typen in unseren Programmen? Und was bringen abhängige und Verfeinerungstypen mit sich?

Andeutungen explizit machen

Ein gemeinsames Thema in der statisch typisierten funktionalen Programmierung ist die explizite Angabe, welche Fehler eine Funktion auslösen kann. Das heißt, anstatt eine Funktion zu haben:

lookupPerson :: Name -> Person

die vielleicht nicht die PersonNotFoundException anspricht, bevorzugen wir etwas in der Art von:

lookupPerson :: Name -> Maybe Person
lookupPerson :: Name -> Either PersonLookupError Person

wobei die Wahl zwischen beiden davon abhängt, ob wir auch zurückmelden wollen, welche Art von Fehler aufgetreten ist.

Ein weiteres wichtiges Anliegen ist die Explizitheit von Seiteneffekten: Wir wollen wissen, ob eine bestimmte Funktion völlig rein ist oder im Gegenteil andere Aktionen im System ausführen kann. Haskell erzwingt diese Trennung; der Typ einer Operation wie das Lesen einer Zeile ist mit IO gekennzeichnet:

readLine :: IO String

In anderen funktionalen Sprachen, wie Scala oder Kotlin, wird diese Trennung nicht vom Compiler erzwungen. Allerdings wird sie von den Bibliotheken zunehmend unterstützt, wie z.B. bei Cats Effect oder Arrow Fx. Es gibt sogar einen Trend, diese binäre Unterscheidung zwischen "rein" und "mit Nebeneffekten" in kleinere Teile zu zerlegen: Sie können eine Funktion als Datenbankabfrage kennzeichnen, aber nichts anderes. Sehen Sie sich Polysemy an, wenn Sie daran interessiert sind.

Die Gemeinsamkeit in diesen Beispielen ist, dass wir einige Informationen über die Funktion explizit gemacht haben, indem wir Typen verwendet haben: Maybe und IO sind Warnzeichen für "mögliche Fehler" oder "kann Seiteneffekte haben". Obwohl dies bereits einen gewissen Wert als Dokumentation hat, besteht der Hauptgewinn darin, dass der Compiler mehr Prüfungen durchführen kann, um sicherzustellen, dass wir die Warnungen nicht übergangen haben. So können wir zum Beispiel nicht mit der Arbeit an Person fortfahren, die wir von lookupPerson erhalten haben, bis wir herausgefunden haben, ob sie erfolgreich war oder nicht:

case lookupPerson "Alex" of
  Nothing -> ... -- something went wrong
  Just p  -> ... -- here we have our Person

Das ist das ganze Spiel. Je mehr Eigenschaften über unsere Daten oder unser Verhalten wir mit unseren Typen ausdrücken können, desto mehr können diese automatisch vom Compiler erzwungen werden. Sie sind auch grenzüberschreitend: Während Unit- oder Integrationstests in der Regel von der Umgebung abhängen, in der die Funktion getestet wird, gelten die durch Typen ausgedrückten Eigenschaften auch dann noch, wenn Sie Ihre Funktionen zu größeren Komponenten zusammensetzen.

Lassen Sie mich Ihnen ein drittes Beispiel dafür geben, was wir mit einem einfachen "type tag" erreichen können. Bei der Arbeit mit eingehenden Daten ist es häufig erforderlich, diese zu bereinigen. Denken Sie an das Escaping von Zeichenketten, die Teil einer SQL-Abfrage sind, oder an spezielle Symbole in HTML. Dieses Tag wird geändert, sobald wir eine spezielle Funktion aufrufen:

sanitize :: Input NotSanitized -> Input Sanitized

Wenn wir außerdem bei der Erstellung unserer HTML-Ansichten nur Eingaben vom Typ Input Sanitized zulassen, können wir ganz sicher sein, dass die Bereinigung stattgefunden hat.

Abhängigkeiten zwischen Werten

Diese Sichtweise auf Typen kann uns bei der Durchsetzung von Eigenschaften in einem Programm recht weit bringen und hat es auch getan. Aber sie greift zu kurz, wenn wir über Beziehungen oder Abhängigkeiten zwischen Werten sprechen wollen. Nehmen wir eine Indizierungsfunktion, die eine Liste oder ein Array und eine Position erhält: Ob ein solcher Aufruf korrekt ist, hängt davon ab, ob die Position innerhalb der Grenzen des Arrays liegt, eine Beziehung zwischen den beiden Eingaben.

LiquidHaskell (eine Erweiterung von Haskell) und Agda (eine Sprache, mit der LiquidHaskell einen großen Teil der Syntax teilt) ermöglichen es uns, diese Beziehung auf unterschiedliche Weise zu schreiben (ich werde später auf die beiden Agda-Sprachen eingehen). Das Wichtigste ist, dass wir den Argumenten Namen geben (xs für die Liste, n für den Index), damit wir später über ihre Beziehung sprechen können.

-- LiquidHaskell
get :: (xs : [a]) -> { n : Int | 0 <= n && n < length xs } -> { v : a | v elem xs }
-- Agda intrinsic
get :: (xs : List a l) -> Fin l -> a
-- Agda extrinsic
get :: (xs : List a l) -> (n : Nat) -> (inBounds n l) -> a

Funktionen sind ein natürlicher Ort, um Abhängigkeiten einzuführen, aber sie sind nicht der einzige. Wir könnten uns einen Typ Sorted a für sortierte Listen vorstellen: In diesem Fall muss der Konstruktor "one more" sicherstellen, dass der neue Wert kleiner ist als der Rest der Liste.

Zweieinhalb Geschmacksrichtungen

Dies ist der Punkt, in dem sich Verfeinerungs- und abhängige Typsysteme unterscheiden. Beginnen wir mit Ein-Satz-Zusammenfassungen:

• Verfeinerung von Typsystemen: "Jeder Typ hat eine zugehörige logische Formel",
• Abhängige Typsysteme: "Werte können auch in Typen erscheinen".

"Logische Formel" ist nur eine schicke Umschreibung für "Boolescher Ausdruck". Im vorherigen Beispiel ist 0 <= n && n < length xs die Formel, die den einfachen Typ Int verfeinert, indem sie Beschränkungen für den Wert angibt. Ein Compiler wie LiquidHaskell ist in der Lage, die Beschränkungen jedes Wertes zu verfolgen, um zu überprüfen, ob jede Invariante eingehalten wird. Wenn wir zum Beispiel schreiben:

if n >= 1 then get lst n else ...

im Zweig then sind wir sicher, dass n einen verfeinerten Typ { n : Int | n >= 1 } hat. Wenn wir es an get weitergeben, erfüllen wir die erste Eigenschaft (da >= 1 zu sein impliziert, >= 0 zu sein), aber wir würden einen Fehler erhalten, da n <= length lst nicht überprüft werden kann.

In einem abhängigen Typsystem können Sie die Länge einer Liste zu einer intrinsischen Eigenschaft der Liste machen. In diesem Fall würde [1, 2] den Typ List Int 2 haben, wobei 2 die tatsächliche Zahl 2 ist! Werte als Typen zu haben ist notwendig, weil wir später über den Wert selbst sprechen wollen. Diese Fähigkeit eröffnet auch die Möglichkeit, Funktionsaufrufe in Typen zu haben, so dass Sie den Typ einer Funktion wie listAppend ausdrücken können, bei der die Länge der resultierenden Liste die Summe der Eingabelängen ist.

listAppend :: List a n -> List a m -> List a (n + m)

Auf die Frage, wie Invarianten durchgesetzt werden können, gibt es bei abhängigen Typen zwei Antworten. Wie wir bereits erklärt haben, können wir intrinsische Eigenschaften haben, was bedeutet, dass ein "falscher" Wert überhaupt nicht konstruiert werden kann. Das ist der Ansatz, den wir verfolgen, wenn wir Fin n schreiben: Hier ist Fin ein Typ, der so definiert ist, dass er nur Werte von 0 bis n - 1 annehmen kann; genau die, die von get akzeptiert werden.

Es gibt noch eine andere Möglichkeit, nämlich eine beliebige Eingabe für n zuzulassen, dann aber einen zusätzlichen Beweis dafür zu verlangen, dass n innerhalb der Grenzen liegt; dies nennt man den extrinsischen Ansatz. Es ist hier nicht der richtige Ort, um ins Detail zu gehen, aber Sie schreiben einen Datentyp , der die gewünschte Beziehung zwischen den Werten kodiert. Auf diese Weise wandeln wir ein Problem, das einer Verfeinerung ähnelt, in unseren Rahmen um.

Dem Compiler etwas beweisen

An einem bestimmten Punkt der Diskussion können Sie lesen:

da Sein >= 1 impliziert, dass Sein >= 0 ist

Aber woher weiß der Computer, dass dies der Fall ist? Einige Compiler versuchen, diese Art des logischen Denkens so weit wie möglich zu automatisieren, indem sie SMT-Solver verwenden. SMT-Solver sind magische Werkzeuge, die entscheiden können, ob eine Formel wahr ist oder ein Gegenbeispiel liefert, und zwar für eine begrenzte Anzahl von Datentypen, einschließlich Zahlen und Mengen. Aber da die meisten Eigenschaften in diese Kategorien fallen, sind sie von unschätzbarem Wert für uns. Die andere Möglichkeit besteht darin, mit Hilfe einer formalen Sprache manuell zu erklären, warum etwas wahr ist.

Bei Verfeinerungstypen ist die Automatisierung die bevorzugte Option, während bei abhängigen Typsystemen das Schreiben von Beweisen von Hand das A und O ist. Beachten Sie jedoch, dass die Automatisierung begrenzt ist. Daher ist es auch bei der Verwendung von Verfeinerungstypen nützlich zu wissen, wie man Beweise schreibt.

Das archetypische Beispiel dafür, dass der Compiler "nichts sehen kann", ist die Tatsache, dass die zweimalige Anwendung von reverse die ursprüngliche Liste ergibt. Wir können diese Eigenschaft in beiden Systemen als Funktion schreiben:

-- LiquidHaskell
revRev :: (lst : [a]) -> { Proof | reverse (reverse lst) == lst }
-- Agda
revRev :: (lst : List a) -> reverse (reverse lst) ≡ lst

Dieses Beispiel zeigt auch eine weitere interessante Eigenschaft dieser Systeme: Sie können Invarianten nicht nur beim Schreiben einer Funktion prüfen, sondern auch in einem separaten Schritt. Dies könnte getan werden, um den ursprünglichen Code nicht aufzublähen, aber auch als Möglichkeit, zusätzliche Eigenschaften zu spezifizieren oder sogar einige (Eigenschafts-)Tests zu ersetzen!