agda - 为什么下面的 Agda 代码不进行类型检查?
问题描述
我是 Agda 的新手,对此感到困惑。
open import Data.Vec
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Fin hiding (_+_ ; splitAt)
open import Data.Product
open import Relation.Binary.PropositionalEquality
difference : ∀ m (n : Fin m) → ∃ λ o → m ≡ toℕ n + o
difference zero ()
difference (suc m) zero = suc m , refl
difference (suc m) (suc n) with difference m n
difference (suc m) (suc n) | o , p1 = o , cong suc p1
takeFin : ∀ {A : Set} {m : ℕ} (n : Fin m) → Vec A m → Vec A (toℕ n)
takeFin {A} {m = m} n vec with difference m n
... | o , p rewrite p with splitAt (toℕ n) vec
... | xs , _ , _ = xs
takeFin 函数给出错误消息:m != lhs of type ℕ 当检查类型 {m : ℕ} (n : Fin m) (o : ℕ) (p : m ≡ toℕ n + o) (lhs : ℕ ) → lhs ≡ toℕ n + o → {A : Set} (vec : Vec A lhs) → Vec A (toℕ n) 生成的 with 函数是良构的
但以下函数确实编译
takeFin' : ∀ {A : Set} {m : ℕ} (n : Fin m) → Vec A m → Vec A m
takeFin' {A} {m = m} n a vec with difference m n
... | o , p rewrite p with splitAt (toℕ n) vec
... | xs , ys , _ = xs ++ ys
takeFin'' : ∀ {A : Set} {m : ℕ} (n : Fin m) → A → Vec A m → Vec A (toℕ n)
takeFin'' {A} {m = m} n a vec = replicate a
谁能帮我吗?
解决方案
正如新的 Agda 用户所倾向于做的那样,您确实使事情变得比您需要的要复杂得多。您打算证明的内容实际上可以以更简单的方式完成,如下所示:
open import Data.Vec
open import Data.Fin
takeFin : ∀ {a} {A : Set a} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {n = zero} (x ∷ v) = []
takeFin {n = suc _} (x ∷ v) = x ∷ takeFin v
您应该始终尝试编写简单的归纳证明,而不是使用不必要的中间引理。
至于为什么您的版本不进行类型检查(它不是编译,它是类型检查),原因在于您的 rewrite 调用是在m ≡ toℕ n + o
您的目标是类型Vec A (toℕ n)
并且不包含任何出现的元素上进行的m
。相反,您要做的是vec
在您的上下文中转换类型,而rewrite
仅针对目标进行操作。以下是我如何使它工作:
takeFin : ∀ {A : Set} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {m = m} {n} vec with difference m n
... | _ , p = proj₁ (splitAt (toℕ n) (subst (Vec _) p vec))
它可以工作,但正如您所见,它远没有那么优雅(而且它还需要difference
您定义的函数),更重要的是,它使用subst
了通常不鼓励使用的方法。
作为旁注,主要是为了好玩,可以使函数更简洁和优雅(但不太容易理解),如下所示:
open import Function
takeFin : ∀ {A : Set} {m} {n : Fin m} → Vec A m → Vec A (toℕ n)
takeFin {n = n} = proj₁ ∘ (splitAt (toℕ n)) ∘ (subst (Vec _) (proj₂ (difference _ n)))
这个版本虽然阅读起来要复杂得多,但显示了 Agda 在推断参数值方面的强大功能,因为只有n
明确给出。
推荐阅读
- java - 学生投票写入文件和读取文件
- ionic3 - 如何更改数据库存储点而不是此链接,数据应存储到我的本地主机
- mingw - 无法在 Mingw 上进行 fltk
- javascript - 在反应状态下使用复杂对象是不是很糟糕?
- amazon-web-services - 如何从我的服务器中删除 .pem 安全检查 (AWS AMAZON)
- java - 传递一个带有lamba表达式的函数来创建一个泛型函数
- parsing - 解析json源时如何查看是哪一行导致了异常?
- java - 将自定义 Java 对象列表转换为数据集会在 Spark 中产生 stackoverflow 异常
- javascript - 如何根据文本字段更改发送 POST 请求?(不使用提交按钮)
- javascript - 如何通过 node_modules 或 bower_components 将完整的 angularjs web 应用程序添加到另一个 web 应用程序项目中?