agda - Agda 如何推断 `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

当把上面的函数翻译成精益时，我震惊地发现它的真实形式实际上就像......

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，我会得到一个关于答案的提示。发生的事情是 Agda 正在做与精益版本相同的事情，即将隐式 arg 包装为suc'd。

这很令人惊讶，因为我认为隐含的参数只是意味着 Agda 应该自己提供它们。我认为当它作为参数传递时它不会改变函数。