Dowody poziomu otwartego typu w Haskell/Idris

Question

W Idris/Haskell można udowodnić właściwości danych poprzez opisywanie typów i używanie konstruktorów GADT, takich jak Vect, jednak wymaga to zakodowania właściwości w typie (np. musi być oddzielnym typem z listy). Czy można mieć typy z otwartym zestawem właściwości (np. Lista zawierająca zarówno długość, jak i przeciętną), na przykład przez przeciążenie konstruktorów lub użycie czegoś w stylu Effect?

Answer 1

Wierzę, że McBride odpowiedział na to pytanie (dla Teorii Typu) w swoim numerze ornament paper (pdf). Koncepcja szukasz jest jedną z algebraicznych ornamentem (Kopalnia nacisk):

algebrą φ opisuje metodę strukturalną interpretowania danych, dając powstanie krotnym cp łączeń acji, stosując metodę rekurencyjnie . Jak można się było spodziewać, wynikowe drzewo połączeń do φ ma taką samą strukturę jak pierwotne dane - w końcu to jest sedno. Ale co, jeśli to było przed wszystkim? Przypuśćmy, że chcemy poprawić wynik krotnie φ z wyprzedzeniem, reprezentując tylko te dane, które podałyby dostarczoną odpowiedź, której szukaliśmy. Powinniśmy potrzebować danych, aby dopasować je do drzewa of wywołań, które dostarcza tę odpowiedź. Czy możemy ograniczyć nasze dane do dokładnie tego? Oczywiście możemy, jeśli indeksujemy według odpowiedzi.

Teraz napiszmy kod. Stworzyłem całość in a gist, ponieważ tutaj będę wstawiać komentarze. Używam również Agdy, ale powinno być łatwe przejście do Idris.

module reornament where 

Zaczynamy od zdefiniowania, co to znaczy być algebra dostarczaniu B s działając na liście A s. Potrzebujemy przypadku podstawowego (wartość typu B), a także sposobu na połączenie nagłówka listy z hipotezą indukcyjną.

ListAlg : (A B : Set) → Set 
ListAlg A B = B × (A → B → B) 

Biorąc pod uwagę tę definicję, możemy zdefiniować typ list A s zaindeksowane przez B s, których wartość jest właśnie wynikiem obliczeń odpowiadającej danej ListAlg A B. W przypadku nil, wynik jest sprawa baza przekazane nam przez algebry (proj₁ alg), podczas gdy w przypadku cons, po prostu połączyć hipotezę indukcyjną z nowej głowy przy użyciu drugiego projekcji:

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 niech importować jakieś biblioteki i zobaczyć kilka przykładów now:

open import Data.Product 
open import Data.Nat 
open import Data.List 

algebra obliczenie długości listy jest podana przez 0 jako sprawy podstawowej i const suc jako sposób połączyć A i długość ogona zbudować długość aktualna lista. Stąd:

AlgLength : {A : Set} → ListAlg A ℕ 
AlgLength = 0 , (λ _ → suc) 

Jeśli elementy są liczbami naturalnymi, wówczas można je zsumować. Algebra odpowiadająca temu stanowi 0 jako podstawowy przypadek i _+_ jako sposób łączenia ℕ wraz z sumą elementów zawartych w ogonie.Stąd:

AlgSum : ListAlg ℕ ℕ 
AlgSum = 0 , _+_ 

Szalona myśl: Jeśli mamy dwa algebry pracujące na tych samych elementach, możemy je połączyć! W ten sposób będziemy śledzić 2 niezmienniki, a nie jedno!

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

An teraz przykłady:

Jeśli śledzisz długość, następnie możemy zdefiniować wektory:

Vec : (A : Set) (n : ℕ) → Set 
Vec A n = ListSpec A AlgLength n 

i mieć, na przykład, to wektor o długości 4:

allFin4 : Vec ℕ 4 
allFin4 = cons 0 (cons 1 (cons 2 (cons 3 nil))) 

Jeśli śledzimy sumę elementów, możemy zdefiniować pojęcie rozkładu: dane statystyczne ibution jest lista prawdopodobieństw, których suma wynosi 100:

Distribution : Set 
Distribution = ListSpec ℕ AlgSum 100 

I możemy określić jednolite jeden na przykład:

uniform : Distribution 
uniform = cons 25 (cons 25 (cons 25 (cons 25 nil))) 

Wreszcie, łącząc długości i sum algebry, możemy realizować ideę o wielkości dystrybucji.

SizedDistribution : ℕ → Set 
SizedDistribution n = ListSpec ℕ (Alg× AlgLength AlgSum) (n , 100) 

I dać ten piękny równomierny rozkład Przez 4 elementów Zestaw:

uniform4 : SizedDistribution 4 
uniform4 = cons 25 (cons 25 (cons 25 (cons 25 nil)))