Agda: il mio codice non digita il controllo (come ottenere argomenti impliciti giusto?)

Question

"checkSimple" ottiene u, un elemento dell'universo U, e controlla se (nat 1) può essere convertito in un tipo di agda dato u. Il risultato della conversione viene restituito.

Ora provo a scrivere un programma di console e ottenere "someU" dalla riga di comando.

Pertanto ho modificato il tipo di "checkSimple" per includere un parametro (u: Maybe U) come parametro (forse perché l'input dalla console può essere "nothing"). Tuttavia non riesco a ottenere il codice per digitare il controllo.

module CheckMain where 


open import Prelude 

-- Install Prelude 
---- clone this git repo: 
---- https://github.com/fkettelhoit/agda-prelude 

-- Configure Prelude 
--- press Meta/Alt and the letter X together 
--- type "customize-group" (i.e. in the mini buffer) 
--- type "agda2" 
--- expand the Entry "Agda2 Include Dirs:" 
--- add the directory 



data S : Set where 
    nat : (n : ℕ) → S 
    nil : S 

sToℕ : S → Maybe ℕ 
sToℕ (nat n) = just n 
sToℕ _  = nothing 


data U : Set where 
    nat  : U 

El : U → Set 
El nat = ℕ 


sToStat : (u : U) → S → Maybe (El u) 
sToStat nat   s = sToℕ s 


-- Basic Test 
test1 : Maybe ℕ 
test1 = sToStat nat (nat 1) 


{- THIS WORKS -} 

checkSimple : (u : U) → Maybe (El u) 
checkSimple someU = sToStat someU (nat 1) 



{- HERE IS THE ERROR -} 

-- in contrast to checkSimple we only get a (Maybe U) as a parameter 
-- (e.g. from console input) 

check : {u : U} (u1 : Maybe U) → Maybe (El u) 
check (just someU) = sToStat someU (nat 1) 
check _ = nothing 


{- HER IS THE ERROR MESSAGE -} 

{- 
someU != .u of type U 
when checking that the expression sToStat someU (nat 1) has type 
Maybe (El .u) 
-} 

Answer 1

La questione è abbastanza semplice in natura: il tipo risultante di sToStat dipende dal valore del suo primo argomento (u : U nel codice); quando in seguito si utilizza sToStat all'interno di check, si desidera che il tipo di reso dipenda da someU - ma check promette che il suo tipo di reso dipende invece dall'implicito u : U!

---

Ora, immaginiamo che questo sia tipografico, ti mostrerò alcuni problemi che potrebbero sorgere.

Cosa succede se u1 è nothing? Bene, in tal caso vorremmo restituire anche nothing. nothing di quale tipo? Maybe (El u) si potrebbe dire, ma ecco la cosa - u è contrassegnato come argomento implicito, il che significa che il compilatore cercherà di dedurlo per noi da un altro contesto. Ma non c'è altro contesto che possa definire il valore di u!

Agda sarà molto probabilmente lamentano metavariables irrisolti ogni volta che si tenta di utilizzare check, il che significa che si deve scrivere il valore di u ovunque si utilizza check, vanificando così il punto di marcatura u implicita, in primo luogo. Nel caso in cui non lo sapeste, Agda ci fornisce un modo per fornire argomenti impliciti:

check {u = nat} {- ... -} 

ma sto divagando.

Un altro problema diventa evidente se si estende U con più costruttori:

data U : Set where 
    nat char : U 

per esempio. Avremo anche per tenere conto di questo caso in più in alcune altre funzioni, ma per lo scopo di questo esempio, diciamo solo avere:

El : U → Set 
El nat = ℕ 
El char = Char 

Ora, qual è check {u = char} (just nat)? sToStat someU (nat 1) è Maybe ℕ, ma El u è Char!

---

E ora per la possibile soluzione. Dobbiamo in qualche modo rendere il tipo di risultato di check dipendente dallo u1. Se abbiamo avuto qualche tipo di unJust funzione, potremmo scrivere

check : (u1 : Maybe U) → Maybe (El (unJust u1)) 

si dovrebbe vedere il problema con questo codice subito - nulla ci garantisce che u1 è just.Anche se restituiremo nothing, dobbiamo comunque fornire un tipo corretto!

Prima di tutto, dobbiamo selezionare un tipo per il caso nothing. Diciamo che vorrei estendere lo U in seguito, quindi devo scegliere qualcosa di neutro. Maybe ⊤ sembra abbastanza ragionevole (solo un promemoria rapido, ⊤ è quello che () è in Haskell - il tipo di unità).

Come possiamo rendere check restituire Maybe ℕ in alcuni casi e Maybe ⊤ in altri? Ah, potremmo usare una funzione!

Maybe-El : Maybe U → Set 
Maybe-El nothing = Maybe ⊤ 
Maybe-El (just u) = Maybe (El u) 

Questo è esattamente ciò di cui avevamo bisogno! Ora check diventa semplicemente:

check : (u : Maybe U) → Maybe-El u 
check (just someU) = sToStat someU (nat 1) 
check nothing  = nothing 

---

Inoltre, questa è l'occasione perfetta per parlare del comportamento riduzione di queste funzioni. Maybe-El è molto sub-ottimale in questo senso, diamo un'occhiata a un'altra implementazione e facciamo un po 'di confronto.

Maybe-El₂ : Maybe U → Set 
Maybe-El₂ = Maybe ∘ helper 
    where 
    helper : Maybe U → Set 
    helper nothing = ⊤ 
    helper (just u) = El u 

O forse noi potremmo risparmiare un po 'di battitura e scrivere:

Maybe-El₂ : Maybe U → Set 
Maybe-El₂ = Maybe ∘ maybe El ⊤ 

Va bene, il precedente e il nuovo Maybe-ElMaybe-El₂ sono equivalenti, nel senso che essi danno stesse risposte per stessi input. Cioè, ∀ x → Maybe-El x ≡ Maybe-El₂ x. Ma c'è un'enorme differenza. Cosa possiamo dire di Maybe-El x senza guardare a ciò che è x? È giusto, non possiamo dire nulla. Entrambi i casi funzione devono sapere qualcosa su x prima di continuare.

Ma che dire di Maybe-El₂? Proviamo lo stesso: iniziamo con Maybe-El₂ x, ma questa volta, possiamo applicare (il solo) caso di funzione. Srotolamento alcune definizioni, si arriva a:

Maybe-El₂ x ⟶ (Maybe ∘ helper) x ⟶ Maybe (helper x) 

E ora siamo bloccati, a causa di ridurre helper x abbiamo bisogno di sapere che cosa è x. Ma guarda, abbiamo ottenuto molto, molto più lontano che con Maybe-El. Fa la differenza?

Consideriamo questa funzione molto stupido:

discard : {A : Set} → Maybe A → Maybe ⊤ 
discard _ = nothing 

Naturalmente, ci si aspetterebbe la seguente funzione a TYPECHECK.

discard₂ : Maybe U → Maybe ⊤ 
discard₂ = discard ∘ check 

check sta producendo Maybe y per qualche y, giusto? Ah, ecco che arriva il problema: sappiamo che è check x : Maybe-El x, ma non sappiamo nulla di x, quindi non possiamo supporre chesi riduca a Maybe y!

Sul lato Maybe-El₂, la situazione è completamente diversa. Noi conosciamo che Maybe-El₂ x si riduce a Maybe y, quindi il discard₂ ora corrisponde ai tipi!