Agda标准库List使用∷ʳ模式匹配报错的技术问询

这个问题的核心原因很明确：_∷ʳ_不是List数据类型的原生构造器，它只是一个定义在List上的辅助函数，因此不能直接用于模式匹配的左侧。

1. 先搞清楚List的本质构造 #

Agda标准库中Data.List.Base里的List类型是这样定义的：

data List {a} (A : Set a) : Set a where
  []  : List A
  _∷_ : A → List A → List A

只有[]（空列表）和_∷_（前置元素构造列表）是合法的数据构造器——模式匹配的左侧只能识别数据构造器，因为它们是用来构建数据类型的“基础砖块”。

2. _∷ʳ_到底是什么？ #

标准库中的_∷ʳ_是一个函数，作用是给列表追加一个末尾元素，它的实现大概是这样：

_∷ʳ_ : ∀ {a} {A : Set a} → List A → A → List A
[]       ∷ʳ x = x ∷ []
(y ∷ ys) ∷ʳ x = y ∷ (ys ∷ʳ x)

它只是一个用来生成列表的工具函数，不是List类型的一部分，所以只能在表达式的右侧用来构建列表，不能在左侧的模式里“拆解”列表。

3. 错误信息里的细节解释 #

你看到的错误里提到了两个_∷ʳ_：一个来自Vec，一个来自List——这是因为Agda在当前作用域里找到了同名的运算符，但不管是哪一个，它们的本质都是函数，不是数据构造器。模式匹配的语法规则只允许用构造器来解构数据，所以Agda无法解析你写的左侧模式。

4. 正确的替代方案 #

如果你想实现“获取除最后一个元素”的功能，有几种可选方式：

• 继续使用你最初的递归实现（也就是allButLast），这是处理普通List的标准写法；
• 利用标准库已经提供的init函数（在Data.List.Base中），它的功能和你的allButLast完全一致；
• 如果需要更严谨地处理非空列表，可以使用Data.List.NonEmpty中的非空List类型，避免空列表的边界情况：

open import Data.List
open import Data.List.NonEmpty

allButLastNonEmpty : ∀ {a} {A : Set a} → List⁺ A → List A
allButLastNonEmpty (x ∷ [])     = []
allButLastNonEmpty (x ∷ y ∷ xs) = x ∷ allButLastNonEmpty (y ∷ xs)

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