我可以使用值的正常形式来避免 Agda 中的不完整模式匹配吗？

Question

在下面的 Agda 程序中，尽管 myList 只适合 cons 的情况，但我收到了关于 one 定义中缺失情况的警告。

open import Data.Nat

data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))

one : ℕ
one with myList 
... | (cons x xs) = x

Incomplete pattern matching for .test.with-16. Missing
cases:
  one | nil

我知道这听起来有点令人费解，但有没有一种方法可以根据 myList 定义 one，而不会将运行变成 "incomplete pattern matching" 错误？

这个例子是我原来的问题的简化，它来自家庭作业，使用了稍微复杂的类型。在那种情况下，"myList" 是一个由小输入的聪明函数计算出的大值。如果我使用 Emacs 的 Agda 模式 (C-c C-n) 计算 "myList" 的正常形式，我可以从中获取 "one" 的值并将其粘贴到我的程序中。然而，这个值在打印出来时需要几十行，所以我在徘徊是否有一种方法可以根据 "myList" 直接定义 "one"，而不会运行进入不完整的模式匹配错误。

Answer 1

如果您使用 with e，那么 e 会从目标和上下文中抽象出来（想想 lambda 抽象），并且您会被要求继续，就好像那里有一个变量而不是 e 本身。因此，以下模式匹配根本没有考虑 myList 的值（相当 counter-intutive，但 with 只是用于创建带有一个额外参数的辅助定义的语法糖）。

然而你可以写下：

open import Agda.Builtin.List
open import Agda.Builtin.Nat renaming (Nat to ℕ)
open import Agda.Builtin.Equality

myList : List ℕ
myList = 1 ∷ 2 ∷ 3 ∷ []

head : {n : ℕ} {ns : List ℕ} (xs : List ℕ) → n ∷ ns ≡ xs → ℕ
head (x ∷ xs) refl = x

one : ℕ
one = head myList refl

您还可以查看标准库中的 inspect 模式以获得更通用的解决此问题的方法。

Answer 2

您可以在类型级别反映一个值，然后对其进行模式匹配。看起来像这样：

open import Data.Nat

data List (A : Set) : Set where
  nil : List A
  cons : A → List A → List A

myList : List ℕ
myList = cons 1 (cons 2 (cons 3 nil))

data Sing {α} {A : Set α} : A -> Set where
  sing : ∀ x -> Sing x

one : ℕ
one with sing myList
... | sing (cons x (cons _ (cons _ nil))) = x

我可以使用值的正常形式来避免 Agda 中的不完整模式匹配吗？

Can I use the normal form of a value to avoid incomplete pattern matches in Agda?

agda