Agda: mi código no escribe check (cómo obtener argumentos implícitos ¿verdad?)

Question

"checkSimple" obtiene u, un elemento del universo U, y comprueba si (nat 1) se puede convertir a un tipo agda dado tú El resultado de la conversión es devuelto.

Ahora trato de escribir un programa de consola y obtener "someU" de la línea de comandos.

Por lo tanto, cambié el tipo de "checkSimple" para incluir un parámetro (u: Maybe U) (tal vez porque la entrada de la consola puede ser "nada"). Sin embargo, no puedo obtener el código para escribir cheque.

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 cuestión es bastante simple en la naturaleza: el tipo resultante de sToStat depende del valor de su primer argumento (u : U en su código); cuando más tarde usa sToStat dentro de check, desea que el tipo de devolución dependa de someU - pero check promete que su tipo de devolución depende del implícito u : U.

---

Ahora, imaginemos que esto no es cierto, le mostraré algunos problemas que podrían surgir.

¿Qué pasa si u1 es nothing? Bueno, en ese caso, nos gustaría devolver nothing también. nothing de qué tipo? Maybe (El u) se podría decir, pero esta es la cuestión: u está marcado como un argumento implícito, lo que significa que el compilador intentará inferirlo para nosotros desde otro contexto. ¡Pero no hay otro contexto que pueda precisar el valor de u!

Agda más probable es que se quejan de metavariables sin resolver cada vez que intente utilizar check, lo que significa que tiene que escribir el valor de todas partes u utiliza check, anulando así el punto de marcar u implícita en el primer lugar. En caso de que no lo sabía, Agda nos da una manera de proporcionar argumentos implícitos:

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

pero estoy divagando.

Otro problema se hace evidente si se amplía U con más constructores:

data U : Set where 
    nat char : U 

por ejemplo. También habrá que tener en cuenta este caso extra en algunas otras funciones, pero para el propósito de este ejemplo, vamos a echar:

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

Ahora, lo que es check {u = char} (just nat)? sToStat someU (nat 1) es Maybe ℕ, pero El u es Char!

---

Y ahora para la posible solución. Necesitamos hacer que el tipo de resultado de check dependa de alguna manera de u1. Si tuviéramos algún tipo de unJust función, podríamos escribir

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

debería ver el problema con este código de inmediato - nada nos garantiza que es u1just.Aunque vamos a devolver nothing, ¡debemos proporcionar el tipo correcto!

En primer lugar, tenemos que elegir algún tipo para el caso nothing. Digamos que me gustaría extender U más tarde, así que tengo que elegir algo neutral. Maybe ⊤ suena bastante razonable (solo un recordatorio rápido, ⊤ es lo que () está en Haskell - el tipo de unidad).

¿Cómo podemos hacer que check devuelva en algunos casos y Maybe ⊤ en otros? Ah, podríamos usar una función!

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

¡Eso es exactamente lo que necesitábamos! Ahora check simplemente se convierte en:

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

---

Además, esta es la oportunidad perfecta para hablar del comportamiento reducción de estas funciones. Maybe-El es muy subóptimo en ese sentido, echemos un vistazo a otra implementación y hagamos un poco de comparación.

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

O tal vez nos podríamos ahorrar algo de escribir y escribir:

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

bien, el anterior y el nuevo Maybe-ElMaybe-El₂ son equivalentes en el sentido que le dan mismas respuestas para mismas entradas. Es decir, ∀ x → Maybe-El x ≡ Maybe-El₂ x. Pero hay una gran diferencia. ¿Qué podemos decir sobre Maybe-El x sin mirar lo que x es? Así es, no podemos decir nada. Ambos casos de funciones necesitan saber algo sobre x antes de continuar.

Pero, ¿qué hay de Maybe-El₂? Probemos lo mismo: comenzamos con Maybe-El₂ x, pero esta vez, podemos aplicar (el único) caso de función. Desenrolla algunas definiciones, llegamos a:

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

Y ahora estamos atascados, porque para reducir helper x necesitamos saber qué es x. Pero mira, tenemos mucho, mucho más lejos que con Maybe-El. ¿Hace alguna diferencia?

considerar esta función muy tonta:

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

Naturalmente, esperaríamos que la función siguiente para typecheck.

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

checkMaybe y está produciendo desde hace algún y, ¿verdad? Ah, aquí viene el problema: sabemos que check x : Maybe-El x, pero no sabemos nada sobre x, por lo que no podemos suponer que Maybe-El x se reduce a Maybe y tampoco!

En el lado Maybe-El₂, la situación es completamente diferente. Nos saber que Maybe-El₂ x se reduce a Maybe y, por lo que el discard₂ ahora tipea!