Agda: mon code ne tape pas check (comment obtenir des arguments implicites?)

Question

"checkSimple" obtient u, un élément de l'univers U, et vérifie si (nat 1) peut être converti en un type agda donné u. Le résultat de la conversion est renvoyé.

Maintenant j'essaye d'écrire un programme de console et d'obtenir "unU" de la ligne de commande.

Par conséquent j'ai changé le type de "checkSimple" pour inclure un (u: Peut-être U) comme paramètre (peut-être parce que l'entrée de la console peut être "rien"). Cependant je ne peux pas obtenir le code pour taper vérifier.

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 question est assez simple dans la nature: le type résultant de sToStat dépend de la valeur de son premier argument (u : U dans votre code); lorsque vous utiliserez plus tard sToStat à l'intérieur de check, vous voulez que le type de retour dépende de someU - mais check promet que son type de retour dépend de l'implicite u : U à la place! Maintenant, imaginons ceci, mais je vais vous montrer quelques problèmes qui pourraient survenir.

Que se passe-t-il si u1 est nothing? Eh bien, dans ce cas, nous aimerions également retourner nothing. nothing de quel type? Maybe (El u) vous pourriez dire, mais voici la chose - u est marqué comme un argument implicite, ce qui signifie que le compilateur essaiera de l'inférer pour nous d'un autre contexte. Mais il n'y a pas d'autre contexte qui définirait la valeur de u!

Agda sera très probablement se plaindre de métavariables non résolues à chaque fois que vous essayez d'utiliser check, ce qui signifie que vous devez écrire la valeur de u partout où vous utilisez check, battant ainsi le point de marquer u implicite en premier lieu. Au cas où vous ne le sauriez pas, Agda nous donne un moyen de fournir des arguments implicites:

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

mais je m'égare.

Une autre question devient évident si vous prolongez U avec plus de constructeurs:

data U : Set where 
    nat char : U 

par exemple. Nous devons aussi tenir compte de ce cas supplémentaire dans quelques autres fonctions, mais dans le but de cet exemple, nous allons avoir simplement:

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

Maintenant, ce qui est check {u = char} (just nat)? sToStat someU (nat 1) est Maybe ℕ, mais El u est Char!

---

Et maintenant pour la solution possible. Nous devons faire en sorte que le type de résultat check dépende de u1. Si nous avions une sorte de fonction unJust, nous pourrions écrire

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

Vous devriez voir le problème avec ce code tout de suite - rien ne nous garantit que u1 est just.Même si nous allons retourner nothing, nous devons toujours fournir un type correct!

Tout d'abord, nous devons choisir un certain type pour le cas nothing. Disons que je voudrais étendre U plus tard, donc je dois choisir quelque chose de neutre. Maybe ⊤ semble assez raisonnable (juste un rappel rapide, ⊤ est ce que () est dans Haskell - le type d'unité).

Comment pouvons-nous check retourner dans certains cas Maybe ℕ et Maybe ⊤ dans d'autres? Ah, nous pourrions utiliser une fonction!

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

C'est exactement ce dont nous avions besoin! Maintenant check devient simplement:

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

---

En outre, c'est l'occasion idéale de mentionner le comportement de réduction de ces fonctions. Maybe-El est très sous-optimale à cet égard, jetons un oeil à une autre mise en œuvre et faire un peu de comparaison.

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

Ou peut-être que nous pourrions nous sauver et écrire quelques frappes:

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

D'accord, le précédent Maybe-El et la nouvelle Maybe-El₂ sont équivalentes dans le sens où ils donnent des réponses aux mêmes mêmes entrées. C'est-à-dire ∀ x → Maybe-El x ≡ Maybe-El₂ x. Mais il y a une énorme différence. Que pouvons-nous dire à propos de Maybe-El x sans regarder ce que x est? C'est vrai, nous ne pouvons rien dire. Les deux cas de fonction doivent savoir quelque chose à propos de x avant de continuer.

Mais qu'en est-il de Maybe-El₂? Essayons la même chose: nous commençons par Maybe-El₂ x, mais cette fois, nous pouvons appliquer (le seul) un cas de fonction. Déroulage quelques définitions, nous arrivons à:

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

Et maintenant nous sommes coincés, parce que pour réduire helper x nous devons savoir ce que x est. Mais regardez, nous avons beaucoup, beaucoup plus loin qu'avec Maybe-El. Est-ce que cela fait une différence?

Tenir compte de cette fonction très stupide:

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

Naturellement, nous nous attendons à la fonction suivante à Typecheck.

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

check est la production Maybe y pour certains y, non? Ah, voici le problème - nous savons que check x : Maybe-El x, mais nous ne savons rien sur , donc nous ne pouvons pas supposer Maybe-El x réduit à Maybe y non plus!

Du côté Maybe-El₂, la situation est complètement différente. Nous sais que Maybe-El₂ x réduit à Maybe y, de sorte que le discard₂ maintenant typechecks!