如何修复Agda中take𝕍函数的不完整模式匹配问题

问题根源 #

你遇到的错误本质是类型签名没有约束输入参数的关系：你的take𝕍类型签名承诺“对于任意自然数m和长度为n的向量，都能返回长度为m的向量”，但当m > n时（比如take𝕍 3 []），逻辑上根本无法构造出长度为m的向量——Agda会严格检查所有可能的输入组合，所以它会提示你缺失take𝕍 (suc m) []这个case。

下面提供两种符合Agda依赖类型逻辑的解决方案，分别对应不同的需求场景：

方案1：限制m ≤ n（仅当m不超过向量长度时生效） #

如果你希望take𝕍只在m小于等于输入向量长度时可用，可以给类型签名添加自然数的小于等于约束，这样从类型层面就排除了m > n的情况，也就不需要处理不可能的take𝕍 (suc m) []了。

首先需要定义自然数的_≤_关系（如果你的库没有的话）：

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

data _≤_ : ℕ → ℕ → Set where
  z≤n : ∀ {n} → zero ≤ n
  s≤s : ∀ {m n} → m ≤ n → suc m ≤ suc n

data 𝕍 (A : Set) : ℕ → Set where
  []  : 𝕍 A zero
  _::_ : ∀ {n} → A → 𝕍 A n → 𝕍 A (suc n)

然后修改take𝕍的实现，加入m ≤ n的证明参数：

take𝕍 : ∀{A : Set}{n : ℕ} → (m : ℕ) → m ≤ n → 𝕍 A n → 𝕍 A m
take𝕍 zero _ []       = []
take𝕍 zero _ (_ :: _) = []
take𝕍 (suc m) (s≤s p) (x :: xs) = x :: take𝕍 m p xs

为什么这样能解决问题？ #

当输入向量是[]（即n=zero）时，m ≤ zero的唯一可能是m=zero——因为suc m ≤ zero没有对应的证明构造子（_≤_的定义里没有这种情况），所以Agda不会要求你处理take𝕍 (suc m) []的模式，模式匹配自然完整。

方案2：返回长度为min m n的向量（兼容m > n的情况，类似Haskell的take） #

如果你想要和Haskell的take行为一致：当m超过向量长度时返回整个向量，那需要调整输出类型为**m和n的最小值**，这样即使m > n，输出的长度也是n，逻辑上可以构造。

首先定义自然数的min函数：

min : ℕ → ℕ → ℕ
min zero n       = zero
min (suc m) zero = zero
min (suc m) (suc n) = suc (min m n)

然后实现take𝕍：

take𝕍 : ∀{A : Set}{n : ℕ} → (m : ℕ) → 𝕍 A n → 𝕍 A (min m n)
take𝕍 zero xs       = []
take𝕍 (suc m) []    = []
take𝕍 (suc m) (x :: xs) = x :: take𝕍 m xs

为什么这样能解决问题？ #

当你调用take𝕍 (suc m) []时，输出类型是𝕍 A (min (suc m) zero)，也就是𝕍 A zero（即空向量），所以返回[]完全符合类型要求，模式匹配也就完整了。

内容的提问来源于stack exchange，提问作者centrinok