为何该Agda程序无法对`with`子句下的表达式进行归一化？

这个问题的核心在于你编写的filter函数在with子句后没有完成完整的模式匹配分支，导致Agda无法确定p x取不同值时函数的行为，自然没办法对相关表达式做归一化处理。

具体原因拆解 #

Agda的with构造是用来根据某个表达式的结果分情况讨论的工具。在你的代码里，with p x表示要根据p x的结果（也就是Bool类型的true或false）来定义filter的行为，但你只写了with p x .....，相当于只提出了分情况的需求，却没有给出任何一种情况的具体处理逻辑。

作为依赖类型语言，Agda要求函数必须是完全定义的——也就是要覆盖所有可能的输入情况。缺少分支的情况下，Agda无法推断出p x为true或false时filter应该返回什么，因此无法对这个表达式进行归一化（也就是把表达式化简到最简形式）。

修正后的完整代码 #

要解决这个问题，你需要为p x的每个可能值添加对应的分支：

module Hello where
data False : Set where
record True : Set where
data Bool : Set where
  true : Bool
  false : Bool
isTrue : Bool -> Set
isTrue true = True
isTrue false = False
satisfies : {A : Set} -> (p : A -> Bool) -> (x : A) -> Set
satisfies p x = isTrue (p x)
data List (a : Set) : Set where
  [] : List a
  _::_ : a -> List a -> List a
filter : {A : Set} -> (A -> Bool) -> List A -> List A
filter p [] = []
filter p (x :: xs) with p x
filter p (x :: xs) | true  = x :: filter p xs  -- 保留符合条件的元素
filter p (x :: xs) | false = filter p xs       -- 过滤掉不符合条件的元素

修正后的逻辑说明 #

• 当p x返回true时，我们把x加入结果列表，再递归过滤剩下的xs；
• 当p x返回false时，我们跳过x，直接递归过滤xs。

现在filter函数有了完整的模式匹配分支，Agda能够明确所有输入情况下的行为，自然就可以对with子句下的表达式进行归一化了。

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