agda - Agda 如何推断 `Vec.foldl` 的隐含参数?
问题描述
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
正确推断出隐含的论点确实令人印象深刻。它是如何做到的?
解决方案
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 应该自己提供它们。我认为当它作为参数传递时它不会改变函数。
推荐阅读
- c++ - 使用 FFMPEG 将 RGB 图像序列保存到 .mp4 时遇到问题
- angular - 下载 url 角度
- file - 内存映射文件真的是文件吗?
- python - 如何在每个计算独立的python中对循环进行多处理?
- c++ - 带有 -stdlib=libc++ 的 clang++ 9.0.1 找不到
- c# - 更改 cmd 的当前工作目录(来自子进程)
- c# - .Net Core 3.1 Web API 在新控制器上抛出 404
- python - Jenkins Dockerfile 构建:[91mstandard_init_linux.go:211:exec 用户进程导致“exec 格式错误”
- python - 为什么总是零作为输出?
- react-native - 我们如何对接 Proton-Native 应用程序并查看 GUI?