Quindi: qual è il punto?

Question

Qual è lo scopo previsto per il tipo So? Traslitterazione in Agda:

data So : Bool → Set where 
    oh : So true 

So solleva una proposta booleano fino ad un uno logico. Il documento introduttivo di Oury e Swierstra The Power of Pi fornisce un esempio di un'algebra relazionale indicizzata dalle colonne delle tabelle. Prendendo il prodotto di due tabelle richiede che essi hanno diverse colonne, per i quali usano So:

Schema = List (String × U) -- U is the universe of SQL types 

-- false iff the schemas share any column names 
disjoint : Schema -> Schema -> Bool 
disjoint = ... 

data RA : Schema → Set where 
    -- ... 
    Product : ∀ {s s'} → {So (disjoint s s')} → RA s → RA s' → RA (append s s') 

io sono abituato a costruire i termini prova per le cose che voglio dimostrare le mie programmi. Sembra più naturale per la costruzione di una relazione logica su Schema s per garantire la sconnessione:

Disjoint : Rel Schema _ 
Disjoint s s' = All (λ x -> x ∉ cols s) (cols s') 
    where cols = map proj₁ 

So sembra avere gravi svantaggi rispetto ad una "corretta" a prova di termine: pattern matching on oh non ti dà alcuna informazione con cui è possibile effettuare un altro controllo di tipo termine (Does?) - che significherebbe valori So non possono partecipare utilmente in prova interattiva. Confrontalo con l'utilità computazionale di Disjoint, che è rappresentata come un elenco di prove che ogni colonna in s' non viene visualizzata in s.

io in realtà non credono che la specifica So (disjoint s s') è più semplice da scrivere rispetto Disjoint s s' - è necessario definire la funzione booleana disjoint senza l'aiuto del tipo-checker - e in ogni caso Disjoint paga per sé quando si desidera manipolare le prove in esso contenute.

Sono anche scettico sul fatto che So consente di risparmiare quando si sta costruendo un Product. Per dare un valore di So (disjoint s s'), è ancora necessario eseguire una corrispondenza di modelli sufficiente su s e s' per soddisfare il correttore di tipi in cui sono effettivamente disgiunti. Sembra uno spreco per scartare le prove così generate.

So sembra ingombrante sia per gli autori che per gli utenti del codice in cui è distribuito. 'Quindi', in quali circostanze vorrei utilizzare So?

Answer 1

Se si dispone già di un b : Bool, è possibile trasformarlo in proposta: So b, che è leggermente più corto di b ≡ true. A volte (non ricordo alcun caso reale) non è necessario preoccuparsi di un corretto tipo di dati, e questa soluzione rapida è sufficiente.

So sembra avere gravi svantaggi rispetto ad una "corretta" a prova di termine: pattern matching on oh non ti dà alcuna informazione con il quale si potrebbe fare un altro tipo di controllo-termine. Come corollario, i valori So non possono partecipare utilmente alla prova interattiva. Contrastare ciò con l'utilità di calcolo di Disjoint, che è rappresentato come un elenco di prove che ogni colonna in s' non è in s.

So ti dà le stesse informazioni Disjoint - basta per estrarlo.Fondamentalmente, se non vi è alcuna incoerenza tra disjoint e Disjoint, allora dovresti essere in grado di scrivere una funzione So (disjoint s) -> Disjoint s usando la corrispondenza del modello, la ricorsione e l'eliminazione di casi impossibili.

Tuttavia, se si ottimizzare la definizione un po ':

So : Bool -> Set 
So true = ⊤ 
So false = ⊥ 

So diventa un tipo di dati molto utile, perché x : So true riduce immediatamente tt a causa della eta-regola per ⊤. Questo permette di utilizzare So come un vincolo: in pseudo-Haskell possiamo scrivere

forall n. (n <=? 3) => Vec A n 

e se n è nella forma canonica (cioè suc (suc (suc ... zero))), quindi n <=? 3 può essere controllato dal compilatore e non sono necessarie prove. In attuale Agda è

∀ {n} {_ : n <=? 3} -> Vec A n 

Ho usato questo trucco in this risposta (è {_ : False (m ≟ 0)} lì). E credo che sarebbe stato impossibile scrivere una versione utilizzabile della macchina di misura descritto here senza questa semplice definizione:

Is-just : ∀ {α} {A : Set α} -> Maybe A -> Set 
Is-just = T ∘ isJust 

dove T è So nella libreria standard del Agda.

Inoltre, in presenza di argomenti istanze So -come-a-tipo di dati possono essere utilizzati come So -come-a-vincolo:

open import Data.Bool.Base 
open import Data.Nat.Base 
open import Data.Vec 

data So : Bool -> Set where 
    oh : So true 

instance 
    oh-instance : So true 
    oh-instance = oh 

_<=_ : ℕ -> ℕ -> Bool 
0  <= m  = true 
suc n <= 0  = false 
suc n <= suc m = n <= m 

vec : ∀ {n} {{_ : So (n <= 3)}} -> Vec ℕ n 
vec = replicate 0 

ok : Vec ℕ 2 
ok = vec 

fail : Vec ℕ 4 
fail = vec