Как Агда выводит неявный аргумент `Vec.foldl`?

Question

foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → B n → A → B (suc n)) →
        B zero →
        Vec A m → B m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs

При переводе вышеупомянутой функции в Lean я был шокирован, обнаружив, что ее истинная форма на самом деле похожа на ...

def foldl : ∀ (P : ℕ → Type a) {n : nat}
    (f : ∀ {n}, P n → α → P (n+1)) (s : P 0)
    (l : Vec α n), P n
| P 0 f s (nil _) := s
| P (n+1) f s (cons x xs) := foldl (fun n, P (n+1)) (λ n, @f (n+1)) (@f 0 s x) xs

Я нахожу действительно впечатляющим, что Agda может вывестинеявный аргумент f правильно. Как это происходит?

Answer 1

foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
        (∀ {n} → B n → A → B (suc n)) →
        B zero →
        Vec A m → B m
foldl b _⊕_ n []       = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (_⊕_ {0} n x) xs

Если я передаю 0 явно, как в версии Lean, я получаю подсказку относительно ответа. То, что происходит, заключается в том, что Agda делает то же самое, что и в версии Lean, а именно оборачивает неявный аргумент arg таким образом, чтобы он был suc 'd.

Это удивительно, поскольку я думал, что неявные аргументы просто означают, чтоАгда должна предоставить их самостоятельно. Я не думал, что это изменит функцию при передаче в качестве аргумента.