Open Level Proofs in Haskell/Idris

Question

In Idris/Haskell, si possono dimostrare le proprietà dei dati annotando i tipi e utilizzando i costruttori GADT, come con Vect, tuttavia, ciò richiede la codifica hard della proprietà nel tipo (ad esempio un Vect deve essere un tipo separato da una lista). È possibile avere tipi con un insieme di proprietà aperte (come la lista che contiene sia una lunghezza che una media corrente), ad esempio sovraccaricando i costruttori o usando qualcosa nella vena di Effetto?

Answer 1

Credo che McBride abbia risposto a questa domanda (per Teoria dei tipi) nel suo ornament paper (pdf). Il concetto che si sta cercando è quello di un ornamento algebrica (sottolineatura mia):

Un φ algebra descrive un metodo strutturale per interpretare i dati, dando luogo a una piega zione oper- φ, applicando il metodo in modo ricorsivo . Non sorprende che l'albero risultante di chiamate a φ abbia la stessa struttura come i dati originali - questo è il punto, dopo tutto. Ma e se questo fosse, prima di tutto, il punto? Supponiamo di voler correggere in anticipo il risultato della piega φ, rappresentando solo quei dati che sarebbero fornire la risposta che volevamo. Dovremmo avere bisogno dei dati per adattarsi a un albero di chiamate φ che fornisca tale risposta. Possiamo limitare i nostri dati a esattamente? Certo che possiamo, se indicizziamo per la risposta.

Ora, scriviamo un po 'di codice. Ho messo l'intera cosa in a gist perché inserirò commenti qui dentro. Inoltre, sto usando Agda ma dovrebbe essere facile da tradurre in Idris.

module reornament where 

Iniziamo definendo ciò che significa essere un algebra fornire B s che agisce su un elenco di A s. Abbiamo bisogno di un caso base (un valore di tipo B) e di unire il capo della lista con l'ipotesi di induzione.

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

Data questa definizione, possiamo definire un tipo di elenchi di A s indicizzati da B s cui valore è precisamente il risultato del calcolo corrispondente ad una determinata ListAlg A B. Nel caso nil, il risultato è il caso base fornita comunicati dalla algebra (proj₁ alg) mentre nel caso cons, semplicemente combinare l'ipotesi di induzione alla nuova testata utilizzando la seconda sporgenza:

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, cerchiamo di importare alcune librerie e vedere un paio di esempi ora:

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

l'algebra calcolare la lunghezza di una lista è data dalla 0 come il caso base e const suc come il modo per combinare un A e la lunghezza della coda per costruire la lunghezza di l'elenco corrente. Quindi:

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

Se gli elementi sono numeri naturali, possono essere sommati. L'algebra corrispondente a quello ha 0 come caso base e _+_ come modo di combinare uno ℕ insieme alla somma degli elementi contenuti nella coda.Quindi:

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

Pazzo pensiero: se abbiamo due algebre che lavorano sugli stessi elementi, possiamo combinarle! In questo modo tracciamo 2 invarianti invece di uno!

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

Un ora gli esempi:

Se stiamo localizzando la lunghezza, allora possiamo definire vettori:

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

e hanno, per esempio, questo vettore di lunghezza 4:

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

Se stiamo monitorando la somma degli elementi, possiamo definire una nozione di distribuzione: un distr ibution è un elenco di probabilità cui somma è 100:

Distribution : Set 
Distribution = ListSpec ℕ AlgSum 100 

E possiamo definire uno uniforme per esempio:

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

Infine, combinando le algebre lunghezza e somma, possiamo implementare la nozione di distribuzione graduata.

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

e dare a questo bel distribuzione uniforme per un 4 elementi di cui:

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