为什么顺序在函数定义中很重要？

Question

给定列表的这些定义：

data List (A : Set) : Set where
    []   : List A
    _::_ : (x : A)(xs : List A) → List A

length : {A : Set} → List A → ℕ
length []        = zero
length (_ :: xs) = suc (length xs)

lookup : {A : Set}(xs : List A)(n : ℕ) → (isTrue (n < length xs)) → A
lookup [] n ()
lookup (x :: xs) zero p = x
lookup (x :: xs) (suc n) p = lookup xs n p

和布尔值：

data Bool : Set where
    true  : Bool
    false : Bool

data False : Set where
record True : Set where

isTrue : Bool → Set
isTrue true     = True
isTrue false    = False

当 _<_ 定义为：

时编译没有错误

open import Data.Nat using (ℕ; suc; zero)

_<_ : ℕ → ℕ → Bool
_     < zero   = false
zero  < suc n  = true
suc m < suc n = m < n

但是如果我将前两个定义的顺序切换为：

_<_ : ℕ → ℕ → Bool
zero  < suc n  = true
_     < zero   = false
suc m < suc n = m < n

然后我得到错误：

isTrue (n < length []) should be empty, but that's not obvious to me
when checking that the clause lookup [] n () has type
{A : Set} (xs : List A) (n : ℕ) → isTrue (n < length xs) → A

这向我暗示 n < length [] 与 zero < suc n = true 匹配，这不应该，因为 length [] 等于 zero 或 suc m < suc n = m < n，这它不应该这样做，因为这是 _<_ 的最后一个定义（以及其他情况的相同推理）。

我是不是误解了 agda 与函数定义的匹配方式，或者这个荒谬的模式是如何工作的？

Answer 1

在内部，Agda 通过模式匹配将定义转换为案例树（请参阅 ReadTheDocs 处的文档）。为了构建这个案例树，Agda 总是首先查看第一个子句。因此，根据子句的顺序，生成的案例树可能会有所不同。在您的示例中， _<_ 的第一个定义的案例树是（伪语法）：

m < n = case n of
          zero   -> false
          suc n' -> case m of
            zero   -> true
            suc m' -> m' < n'

而 _<_ 的第二个定义的案例树是

m < n = case m of
          zero   -> case n of
            zero   -> false
            suc n' -> true
          suc m' -> case n of
            zero   -> false
            suc m' -> m' < n'

实际上，在第二个定义中，Agda 将单个子句 _ < zero = false 拆分为两个子句 zero < zero = false 和 suc m < zero = false，防止 n < zero 进一步减少。

要阻止 Agda 像这样拆分子句，您可以将 {-# OPTIONS --exact-split #-} 放在文件的顶部（或将 --exact-split 添加到 Agda 的命令行标志中）。

如果您想详细了解如何通过模式匹配将定义细化为案例树，您可以阅读 our upcoming ICFP paper 有关该主题的内容。

Answer 2

Jesper 的正确回复还指出了另一种使 lookup 与 _<_ 的第二个定义一起工作的方法：只需自己匹配 n，这样 n 的哪个分支是明确的=12=] 取：

lookup : {A : Set}(xs : List A)(n : ℕ) → (isTrue (n < length xs)) → A
lookup [] zero ()
lookup [] (suc _) ()
lookup (x :: xs) zero p = x
lookup (x :: xs) (suc n) p = lookup xs n p

为什么顺序在函数定义中很重要？

Why does order matter in function definition?

pattern-matching

agda