Open Type Level Proofs in Haskell/Idris

Question

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?

Answer 1

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)))