为什么 Agda 这里需要模式匹配

Question

我有以下内容：

\n

open import Agda.Builtin.Equality\nopen import Agda.Builtin.Nat renaming (Nat to \xe2\x84\x95)\nopen import Agda.Builtin.Sigma\nopen import Agda.Primitive\n\n_\xc3\x97_ : {n m : Level} (A : Set n) (B : Set m) \xe2\x86\x92 Set (n \xe2\x8a\x94 m)\nX \xc3\x97 Y = \xce\xa3 X (\xce\xbb _ \xe2\x86\x92 Y)\n\n\xe2\x84\x95\xc2\xb2 : Set\n\xe2\x84\x95\xc2\xb2 = \xe2\x84\x95 \xc3\x97 \xe2\x84\x95 \n\ncanonical : \xe2\x84\x95\xc2\xb2 \xe2\x86\x92 \xe2\x84\x95\xc2\xb2\ncanonical (x , 0) = (x , 0)\ncanonical (0 , y) = (0 , y)\ncanonical (suc x , suc y) = canonical (x , y)\n\np1 : (a : \xe2\x84\x95) \xe2\x86\x92 (a , 0) \xe2\x89\xa1 canonical (a , 0) -- works\np1 a = refl\n\np2 : (a : \xe2\x84\x95) \xe2\x86\x92 (0 , a) \xe2\x89\xa1 canonical (0 , a) -- doesn't work\np2 a = refl\n\np3 : (a : \xe2\x84\x95) \xe2\x86\x92 (0 , a) \xe2\x89\xa1 canonical (0 , a) -- works\np3 0 = refl\np3 (suc a) = refl\n

\n

当我尝试进行类型检查时，agda 在 p2 中响应错误

\n

zero != fst (canonical (0 , a)) of type \xe2\x84\x95\nwhen checking that the expression refl has type\n(0 , a) \xe2\x89\xa1 canonical (0 , a)\n

\n

为什么 Agda 要求我对一对中的第二个元素进行模式匹配，如 p3 中那样？为什么 p1 进行类型检查而不是 p2 ？

\n

Answer 1

Agda 通过与案例树进行模式匹配来编译所有定义，如函数定义的用户手册页中所述。在您的情况下，案例树如下所示：

canonical xy = case xy of
  (x , y) -> case y of
    zero -> (x , 0)
    suc y -> case x of
      zero -> (0 , suc y)
      suc x -> canonical (x , y)

特别是，只有当第二个参数已知为 或 时，该函数才会zero计算suc。当发生这种情况时，Agda 通过为第二个子句提供浅灰色背景来提供温和的警告。--exact-split您还可以通过打开该标志（{-# OPTIONS --exact-split #-}在文件顶部使用编译指示）将其变成错误。

如果您想了解更多关于案例树的翻译，我推荐我们关于依赖模式匹配的阐述的论文。您可能还对这个问题的可能解决方案感兴趣（遗憾的是它没有进入 Agda 的主版本）或允许您通过首先证明计算规则然后将其注册为重写规则来添加计算规则的--rewriting标志。canonical (0 , y) = (0 , y)