Ich versuche eine Funktion zu schreiben
%Vor% ruft das i-te Element aus einem Vektor der Größe n ab.
Diese Vektoren sind wie folgt definiert:
%Vor% Gibt es eine Möglichkeit, die Funktion getColumn so zu schreiben, dass der Compiler den Code zurückweist, wenn Int für die Größe von Vector zu groß ist?
Wie würde ich diese Funktion schreiben?
Zuerst brauchen wir einen Singleton Typ für die Naturals. Singletons sind Laufzeitdarstellungen von Daten auf Typenebene und werden Singletontypen genannt, da jeder von ihnen nur einen einzigen Wert aufweist. Dies ist nützlich, da es eine Eins-zu-Eins-Entsprechung zwischen den Werten und dem dargestellten Typ herstellt; Wenn wir nur den Typ oder den Wert kennen, können wir auf den anderen schließen.
Damit können wir auch die Einschränkung umgehen, dass Haskell-Typen nicht von Haskell-Werten abhängen können: Unsere Typen hängen vom -Typ-Index eines Singletons ab, aber dieser Typ-Index kann wiederum aus
Wir können sehen, dass für jede n , SNatural n nur einen einzigen möglichen Wert hat; Es spiegelt nur die ursprüngliche Natural -Definition.
Es gibt mehrere Möglichkeiten, wie wir zur Vektorindexierung übergehen können.
< -Restriktion direkt. Das Definieren von < auf Naturals ist einfach:
Jetzt können wir die Begrenztheit mit einer Typgleichheitsbedingung ausdrücken:
%Vor% Dies ist die Standardlösung für die abhängige Typisierung und IMO die einfachere, obwohl sie auf den ersten Blick etwas schwieriger zu verstehen ist. Wir nennen den gebundenen natürlichen Typ Fin n (für "endlich"), wobei n ein natürlicher Wert ist, der die obere Grenze darstellt. Der Trick besteht darin, unsere Zahl so zu indizieren, dass die Größe des Wertes nicht größer als der Index sein kann.
Es ist offensichtlich, dass Fin Zero keine Werte hat. Fin (Succ Zero) hat einen einzelnen Wert, FZero , Fin (Succ (Succ Zero)) hat zwei Werte und somit hat Fin n immer n mögliche Werte. Wir können es für eine sichere Indexierung verwenden:
singletons -Bibliothek und machen Sie eine sichere Indizierung durch Int -s. Wie wir gesehen haben, erfordert die abhängige Programmierung in Haskell eine große Menge an Standardwerten. Die Daten auf Typenebene und ihre Singletons sind mehr oder weniger identisch und benötigen dennoch getrennte Definitionen. Die auf ihnen arbeitenden Funktionen müssen ähnlich dupliziert werden. Zum Glück kann das singletons -Paket das für uns notwendige Muster erzeugen:
Das Paket enthält auch praktische Möglichkeiten, um Singleton-Werte nach Bedarf aus Typen zu generieren:
%Vor% sing ist ein polymorpher Wert, der als Ersatz für einen Singleton-Wert dienen kann. Manchmal kann der korrekte Wert aus dem Kontext abgeleitet werden, aber manchmal müssen wir seinen Typindex mit der Erweiterung ScopedTypeVariables annotieren.
Jetzt können wir auch sicher durch Int -s indizieren, ohne allzu sehr von der Standardtabelle gestört zu sein (nicht eine katastrophale Menge von Boilerplate; die Implementierung von sing für Nat von Hand würde eine erfordern mehr typeclass und ein paar Instanzen).
Im Allgemeinen geht es bei verifizierter Programmierung nicht darum, die Datenkompilierungszeit zu validieren (wie wir in den obigen Beispielen gesehen haben), sondern um Funktionen zu schreiben, die nachweislich korrekt funktionieren, selbst bei unbekannten Kompilierungszeiten ( Sie könnten sagen, dass es irrelevant ist, wenn wir die Daten validieren, vorausgesetzt, dass die Validierungsfunktionen korrekt sind. Unser index kann als semi-verified-Funktion betrachtet werden, weil es unmöglich ist, eine fehlerwerfende Version davon zu implementieren, die typechecks (modulo bottoms and divergence).
Um sicher nach Int -s zu indizieren, müssen wir nur eine verifizierte Konvertierungsfunktion von Int nach Fin schreiben und dann index wie gewohnt verwenden:
Auch hier ist der Zauber von checkBound , dass es unmöglich ist, eine Definition zu schreiben, die ein Fin zurückgibt, das die gegebene Grenze verletzt.
Hier müssen wir einige singletons Maschinen benutzen: Die SingI Bedingung erlaubt es uns einen passenden Singleton Wert mit sing zu erzeugen. Es ist eine harmlose Klassenbeschränkung, weil alle möglich ist n ist eine Instanz von SingI , nach Konstruktion.
Tags und Links haskell