Agda: mein Code nicht Typ prüfen (wie implizite Argumente richtig?)

Question

"checkSimple" bekommt Sie, ein Element des Universums U, und prüft, ob (nat 1) in einen Agda-Typ umgewandelt werden kann u. Das Ergebnis der Konvertierung wird zurückgegeben.

Jetzt versuche ich ein Konsolenprogramm zu schreiben und "someU" von der Kommandozeile zu bekommen.

Deshalb habe ich den Typ von "checkSimple" geändert, um ein (U: Maybe U) als Parameter zu enthalten (vielleicht weil die Eingabe von der Konsole "nichts" sein kann). Allerdings kann ich den Code nicht zur Typüberprüfung bringen.

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

Die Frage ist ganz einfach in der Natur: die resultierende Art von sToStat auf dem Wert ihres ersten Arguments abhängt (u : U in Ihrem Code); Wenn Sie später sToStat innerhalb check verwenden, möchten Sie, dass der Rückgabetyp von someU abhängt - aber check verspricht, dass sein Rückgabetyp von der impliziten u : U stattdessen abhängt!

---

Jetzt stellen wir uns vor, dies tut typecheck, ich werde Ihnen einige Probleme zeigen, die entstehen würden.

Was ist, wenn u1nothing ist? Nun, in diesem Fall möchten wir auch nothing zurückgeben. nothing welcher Art? Maybe (El u) könnte man sagen, aber hier ist die Sache - u ist als implizites Argument markiert, was bedeutet, der Compiler wird versuchen, es für uns aus einem anderen Kontext abzuleiten. Aber es gibt keinen anderen Kontext, der den Wert von u festlegt!

Agda wird höchstwahrscheinlich über ungelöste Metavariablen beschweren, wenn Sie versuchen, check zu verwenden, was bedeutet, dass Sie den Wert von u zu schreiben haben überall Sie check verwenden, also den Punkt zu besiegen u implizit in erster Linie Markierung. Wenn Sie nicht wussten, Agda gibt uns eine Möglichkeit, implizite Argumente zur Verfügung zu stellen:

aber ich schweife ab.

Ein weiteres Problem wird deutlich, wenn man U mit mehr Konstrukteure erweitern:

data U : Set where 
    nat char : U 

zum Beispiel. Wir werden auch für diese zusätzlichen Fall in einigen anderen Funktionen berücksichtigen müssen, aber für die Zwecke dieses Beispiel nehmen wir haben gerade:

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

Nun, was ist check {u = char} (just nat)? sToStat someU (nat 1) ist Maybe ℕ, aber El u ist Char!

---

Und jetzt für die mögliche Lösung. Wir müssen den Ergebnistyp check irgendwie von u1 abhängig machen. Wenn wir eine Art unJust Funktion hatten, konnten wir

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

schreiben Sie sollten das Problem mit diesem Code sofort sehen - nichts garantiert uns, dass u1just ist.Auch wenn wir nothing zurückgeben, müssen wir immer noch einen korrekten Typ angeben!

Zunächst müssen wir einen Typ für den nothing Fall auswählen. Nehmen wir an, ich möchte später U erweitern, also muss ich etwas Neutrales wählen. Maybe ⊤ klingt ziemlich vernünftig (nur eine kurze Erinnerung, ⊤ ist, was () ist in Haskell - der Einheitentyp).

Wie können wir machen check zurück Maybe ℕ in einigen Fällen und Maybe ⊤ in anderen? Ah, wir könnten eine Funktion benutzen!

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

Genau das brauchen wir! Jetzt check einfach wird:

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

---

Auch dies die perfekte Gelegenheit, um die Reduktionsverhalten dieser Funktionen zu nennen. Maybe-El ist in dieser Hinsicht sehr suboptimal, schauen wir uns eine andere Implementierung an und machen ein bisschen Vergleich.

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

Oder vielleicht könnten wir uns etwas Tipp speichern und schreiben:

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

Ordnung, die vorherigen Maybe-El und die neuen Maybe-El₂ sind in dem Sinne äquivalent, dass sie dieselben Antworten für gleiche Eingänge geben. Das heißt ∀ x → Maybe-El x ≡ Maybe-El₂ x. Aber es gibt einen großen Unterschied. Was können wir über Maybe-El x sagen, ohne zu schauen, was x ist? Das stimmt, wir können nichts sagen. Beide Funktionsfälle müssen etwas über x wissen, bevor Sie fortfahren.

Aber was ist mit Maybe-El₂? Lassen Sie uns das gleiche versuchen: Wir beginnen mit Maybe-El₂ x, aber dieses Mal können wir (den einzigen) Funktionsfall anwenden. Abrollen einige Definitionen, kommen wir zu:

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

Und jetzt sind wir fest, weil helper x wir wissen müssen, zu reduzieren, was x ist. Aber schau, wir haben viel, viel weiter als mit Maybe-El. Macht es einen Unterschied?

Betrachten Sie diese sehr dumme Funktion:

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

Natürlich würden wir erwarten, die folgende Funktion typecheck.

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

check produziert Maybe y für einige y, nicht wahr? Ah, hier kommt das Problem - wir wissen, dass check x : Maybe-El x, aber wir wissen nichts über x, so können wir nicht davon ausgehen, Maybe-El x reduziert auf Maybe y entweder!

Auf der Seite Maybe-El₂ ist die Situation völlig anders. Wir wissen, dass Maybe-El₂ x auf Maybe y reduziert, so dass die discard₂ jetzt typechecks!