这是来自自定义 agda 库的代码。在下面的代码中，????代表向量，ℕ 代表自然数。采取？？？？类型类似于 Haskell。示例：“取 3 [1,2,3,4,5,6,7,8]”导致 [1,2,3]。
take???? : ∀{A : Set}{n : ℕ} → (m : ℕ) → ???? A n → ???? A m
take???? 0 xs = []
take???? (suc m) (x :: xs) = x :: take???? m xs
我不断收到错误：
take????的不完整模式匹配。缺失案例：
拿？？？？ （如 m) [] 检查take的定义时？？？？
我不明白，我可能会错过什么可能的证据。
【问题讨论】：
标签： functional-programming agda
take? 的类型签名表明，对于任何完全不受约束的m，您可以返回一个长度为m 的Vec，而Vec 的长度为n。这当然不是真的，因为m 必须小于或等于n，因为您想返回Vec 的前缀。由于要采用的许多元素和 Vec 的长度彼此无关，因此 Agda 会为您提供有关不完整模式匹配的错误。
在 Agda 标准库中，m 小于或等于输入长度 Vec 的限制表示如下：
take : ∀ {a} {A : Set a} m {n} → Vec A (m + n) → Vec A m
你也可以定义类似的东西
take : ∀ {a} {A : Set a} {m n} → m ≤ n → Vec A n → Vec A m
甚至
take : ∀ {a} {A : Set a} m {n} → Vec A n → Vec A (m ⊔ n)
对Data.List.take 的行为进行建模（其中_⊔_ 在Agda 标准库中表示min）。
【讨论】：
您正在对m 和? A n 类型的向量xs 进行模式匹配。不能保证，因为m 是suc-headed，所以xs 是非空的。正如错误提示的那样，您还需要考虑m 为suc 而xs 为空的情况。
或者，您可以编写一个具有更精确类型的函数，以保证xs 至少与m 一样长。这是标准库中使用的：
take : ∀ {A : Set} m {n} → Vec A (m + n) → Vec A m
【讨论】：