In Idris/Haskell kann man Eigenschaften von Daten beweisen, indem man die Typen annotiert und GADT Konstruktoren benutzt, wie zB mit Vect, dies erfordert jedoch eine Festkodierung der Eigenschaft in den Typ (zB ein Vect muss ein separater Typ von einer Liste sein). Ist es möglich, Typen mit einem offenen Satz von Eigenschaften (z. B. Liste, die sowohl eine Länge als auch einen laufenden Durchschnitt enthält) zu haben, z. B. durch Überladen von Konstruktoren oder durch Verwendung von etwas in der Wirkungsrichtung?Open Type Level Proofs in Haskell/Idris
Antwort
Ich glaube, dass McBride diese Frage (für Type Theory) in seiner ornament paper (pdf) beantwortet hat. Das Konzept Sie suchen, ist derjenige einer algebraischen Ornament (Hervorhebung von mir):
Eine Algebra φ beschreibt eine strukturelle Methode Daten zu interpretieren, was zu einer Falte φ oper- ation, die Anwendung des Verfahrens rekursiv . Es überrascht nicht, dass der resultierende Baum der Aufrufe von φ die gleiche Struktur wie die Originaldaten hat - das ist der Punkt schließlich. Aber Was wäre, wenn das vor allem der Punkt wäre? Angenommen, wir wollten das Ergebnis von Faltung φ im Voraus korrigieren, indem wir nur die Daten darstellen, die die von uns gewünschte Antwort liefern würden. Wir sollten die Daten benötigen, um mit einem Baum von φ-Aufrufen zu passen, der diese Antwort liefert. Können wir unsere Daten auf genau das beschränken? Natürlich können wir das, wenn wir nach der Antwort indexieren.
Jetzt wollen wir etwas Code schreiben. Ich habe das ganze Ding in a gist gesetzt, weil ich hier Kommentare verschachteln werde. Außerdem verwende ich Agda, aber es sollte leicht sein, zu Idris zu übersetzen.
module reornament where
Wir beginnen mit der Definition dessen, was es bedeutet, eine Algebra liefert B
s Handeln auf einer Liste von A
s zu sein. Wir benötigen einen Basisfall (einen Wert vom Typ B
) sowie eine Möglichkeit, den Kopf der Liste mit der Induktionshypothese zu kombinieren.
ListAlg : (A B : Set) → Set
ListAlg A B = B × (A → B → B)
Diese Definition gegeben, können wir eine Art von Listen von A
s indiziert durch B
s, dessen Wert genau das Ergebnis der Berechnung entsprechend einem gegebenen ListAlg A B
definieren. Im nil
Fall das Ergebnis ist das Basismodell, die von der Algebra zur Verfügung gestellt (proj₁ alg
), während im cons
Fall haben wir einfach die Induktionsvoraussetzung mit dem neuen Leiter verbinden die zweite Projektion:
data ListSpec (A : Set) {B : Set} (alg : ListAlg A B) : (b : B) → Set where
nil : ListSpec A alg (proj₁ alg)
cons : (a : A) {b : B} (as : ListSpec A alg b) → ListSpec A alg (proj₂ alg a b)
Ok, lassen Sie uns einige Bibliotheken importieren und ein paar Beispiele sehen jetzt:
open import Data.Product
open import Data.Nat
open import Data.List
die Algebra die Länge einer Liste der Berechnung wird von 0
als Basisfall und const suc
als Weg gegeben eine A
und die Länge des Schwanzes zu kombinieren um die Länge von zu bauen die aktuelle Liste. Daher:
AlgLength : {A : Set} → ListAlg A ℕ
AlgLength = 0 , (λ _ → suc)
Wenn die Elemente natürliche Zahlen sind, können sie summiert werden. Die entsprechende Algebra hat 0
als Basisfall und _+_
als die Möglichkeit, einen ℕ
zusammen mit der Summe der im Schwanz enthaltenen Elemente zu kombinieren.Also:
Verrückter Gedanke: Wenn wir zwei Algebren haben, die an den gleichen Elementen arbeiten, können wir sie kombinieren! Auf diese Weise werden wir 2 Invarianten statt 1 verfolgen!
Alg× : {A B C : Set} (algB : ListAlg A B) (algC : ListAlg A C) →
ListAlg A (B × C)
Alg× (b , sucB) (c , sucC) = (b , c) , (λ a → λ { (b , c) → sucB a b , sucC a c })
Ein jetzt die Beispiele:
Wenn wir die Länge verfolgen, dann können wir Vektoren definieren:
Vec : (A : Set) (n : ℕ) → Set
Vec A n = ListSpec A AlgLength n
Und haben, zum Beispiel diesen Vektor der Länge 4:
allFin4 : Vec ℕ 4
allFin4 = cons 0 (cons 1 (cons 2 (cons 3 nil)))
Wenn wir die Summe der Elemente verfolgen, können wir einen Verteilungsbegriff definieren: eine statistische Verteilung ibution ist eine Liste von Wahrscheinlichkeiten, deren Summe 100:
Distribution : Set
Distribution = ListSpec ℕ AlgSum 100
Und wir können ein einheitlich man zum Beispiel definieren:
uniform : Distribution
uniform = cons 25 (cons 25 (cons 25 (cons 25 nil)))
Schließlich wird durch die Länge und die Summe algebras Kombination wir den Begriff umsetzen können von Größenverteilung.
SizedDistribution : ℕ → Set
SizedDistribution n = ListSpec ℕ (Alg× AlgLength AlgSum) (n , 100)
Und geben Sie diese schöne gleichmäßige Verteilung für ein 4-Elemente festgelegt:
uniform4 : SizedDistribution 4
uniform4 = cons 25 (cons 25 (cons 25 (cons 25 nil)))
- 1. Sind type family instance proofs möglich?
- 2. Type-Level-Sets in Haskell/Agda
- 3. Wie Open Type Fonts in Java zu verwenden?
- 4. Open Type (Strg + Umschalt + T) in Eclipse aus jedem Fenster
- 5. Was ist der Unterschied zwischen "Open Type"/"Open Resource" in Eclipse?
- 6. Was ist das Haskell Syntax (type level operators?)
- 7. Open-Source-Bildverarbeitungsbibliothek, die High-Level-3D-Algorithmen unterstützt?
- 8. So installieren Sie Open Type Fonts mit Wix
- 9. Rendern von PDF-Proofs mit Java (via LaTex?)
- 10. Type Level Literals - Kann nicht anders typisierte Parameter in der binären Funktion verwenden
- 11. Was sind TYPE, TYPES, TYPE-POOL, TYPE-POOLS und TYPE-GROUP in SAP/ABAP?
- 12. ..level .. in ggplot2 Konturplot
- 13. Ist es möglich, in SQL Reporting Services (2008) Open Type-Schriftarten (.otf) zu verwenden
- 14. Scala type lowerbound bug?
- 15. Convert type-level list '[a, b, c, ...] zu funktionieren a-> b-> c->
- 16. Servant API type level routing mit typeclasses - howto wählen instanz auf wahl (: <|>)?
- 17. Wie funktioniert HTML5 input type E-Mail ohne Top-Level-Domain-Namen arbeitet
- 18. Bottom Type in Swift
- 19. elastische Suche in verschachtelten Multi-Level-Objekt
- 20. Open Source verwaltete Programmiersprachen
- 21. Warum static_cast <Type> (Objekt) kopiert Objekt in Type?
- 22. Disable particluar level in log4net
- 23. Triple-Level-Assoziationen in phpactivecord
- 24. Nameerror in Multi-Level-Paket
- 25. Log-Level in Unittest ändern
- 26. Multi-Level-Gruppierung in LINQ?
- 27. Multi-Level-Virtualisierung in WPF
- 28. JAXB: Paket.Paket. <Type> ist bereits in package.package definiert. <Type>. <Type>
- 29. Generic Method Type Sicherheit
- 30. Handle Application-Level Fehler
Das ist brillant. Ich schrieb eine Idris-Übersetzung: https://gist.github.com/puffnfresh/35213f97ec189757a179 –