Agda: mój kod nie sprawdza typu (jak uzyskać niejawne argumenty poprawnie?)

Question

"checkSimple" pobiera u, element wszechświata U, i sprawdza, czy (nat 1) można przekonwertować na typ agda podany u. Wynik konwersji jest zwracany.

Teraz próbuję napisać program konsoli i pobrać "someU" z wiersza poleceń.

Dlatego zmieniłem typ "checkSimple", aby uwzględnić parametr (u: Maybe U) (może dlatego, że dane wejściowe z konsoli mogą być "nic"). Jednak nie mogę uzyskać kodu do sprawdzenia typu.

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

Problem jest dość prosty w naturze: otrzymany rodzaj sToStat zależy od wartości swojego pierwszego argumentu (u : U w kodzie); gdy później użyjesz sToStat wewnątrz check, chcesz, aby typ zwracany był zależny od someU - ale check obiecuje, że jego typ zwracany jest w zamian za niejawnym u : U!

---

Wyobraźmy sobie teraz, że to sprawdzenie, pokażę wam kilka problemów, które mogą się pojawić.

Co zrobić, jeśli u1 jest nothing? Cóż, w tym przypadku chcielibyśmy również zwrócić nothing. nothing jakiego typu? Maybe (El u) możesz powiedzieć, ale o to chodzi - u jest oznaczony jako niejawny argument, co oznacza, że ​​kompilator spróbuje wywnioskować go dla nas z innego kontekstu. Ale nie ma innego kontekstu, który pozwoliłby ustalić wartość u!

Agda najprawdopodobniej narzekać nierozwiązanych metavariables gdy spróbujesz użyć check, co oznacza, że ​​trzeba pisać wartość u wszędzie użyć check, tym samym pokonując punkt znakowania u niejawny w pierwszej kolejności. W przypadku, gdybyś nie wiedział, Agda podaje nam sposób dorozumianej argumentacji:

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

ale dygresja.

Kolejną kwestią staje się oczywiste, jeśli przedłużyć U z kilku konstruktorów:

data U : Set where 
    nat char : U 

na przykład. Będziemy mieć również do odpowiedzialności za to dodatkową w przypadku kilku innych funkcji, ale dla celów tego przykładu, niech po prostu:

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

Teraz, co jest check {u = char} (just nat)? sToStat someU (nat 1) jest Maybe ℕ, ale El u jest Char!

---

A teraz możliwe rozwiązanie. Musimy w jakiś sposób sprawić, aby typ wyniku check zależał od u1. Gdybyśmy mieli jakąś unJust funkcji, moglibyśmy napisać

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

powinien pojawić się problem z tym kodem od razu - nic nie gwarantuje nam, że u1 jest just.Mimo że zamierzamy zwrócić nothing, musimy podać poprawny typ!

Po pierwsze, musimy wybrać rodzaj dla przypadku nothing. Powiedzmy, że chciałbym później rozszerzyć U, więc muszę wybrać coś neutralnego. Maybe ⊤ brzmi całkiem rozsądnie (tylko szybkie przypomnienie, ⊤ jest tym, co () jest w Haskell - typ jednostki).

Jak możemy w niektórych przypadkach zwrócić checkMaybe ℕ i Maybe ⊤ w innych? Ach, możemy użyć funkcji!

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

Dokładnie tego potrzebowaliśmy! Teraz check staje się po prostu:

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

---

Ponadto, jest to doskonała okazja, aby wspomnieć o zachowanie redukcji tych funkcji. Maybe-El jest bardzo nieoptymalny pod tym względem, spójrzmy na inną implementację i zróbmy trochę porównania.

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

A może moglibyśmy zaoszczędzić nam trochę pisać i pisać:

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

Alright, poprzedni Maybe-El a nowy Maybe-El₂ są równoważne w sensie, że dają takie same odpowiedzi na samych wejściach. To znaczy ∀ x → Maybe-El x ≡ Maybe-El₂ x. Ale jest jedna ogromna różnica. Co możemy powiedzieć o Maybe-El x bez patrzenia na to, co to jest x? Tak, nie możemy nic powiedzieć. Oba przypadki funkcji muszą wiedzieć coś o x przed kontynuowaniem.

Ale co z Maybe-El₂? Spróbujmy tego samego: zaczynamy od Maybe-El₂ x, ale tym razem możemy zastosować (jedyny) przypadek funkcji. Rozwijając kilka definicji, otrzymujemy:

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

A teraz jesteśmy zatrzymany, ponieważ zmniejszenie helper x musimy wiedzieć co x jest. Ale zobacz, mamy dużo, znacznie dalej niż z Maybe-El. Czy to robi różnicę?

Rozważmy to bardzo głupie funkcję:

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

Oczywiście, moglibyśmy oczekiwać następujących funkcji do typecheck.

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

check produkuje Maybe y jakiegoś y, prawda? Ach, nadchodzi problem - wiemy, że check x : Maybe-El x, ale nie wiemy nic na temat x, więc nie możemy zakładać, że Maybe-El x redukuje się do Maybe y!

Po stronie Maybe-El₂ sytuacja wygląda zupełnie inaczej. Mamy wiem że Maybe-El₂ x zmniejsza się do Maybe y, więc discard₂ teraz typechecks!