Agda自定义语法声明规则咨询：双变量Lambda绑定报错原因

我之前也在Agda自定义语法的多变量绑定这儿卡过，刚好能解答你的问题！

首先得明确Agda syntax声明的核心限制：语法左侧的Lambda表达式只能绑定单个变量，你写的λ x y → body这种多变量缩写形式，Agda的语法解析器是不识别的——这就是你报错的直接原因。

为什么单变量能行，双变量不行？ #

你成功的twice示例里，λ x → body是标准的单变量Lambda绑定，完全符合syntax的解析规则。但当你尝试λ x y → body时，Agda会把y当成Lambda体的起始部分，而不是第二个绑定变量，自然就抛出解析错误了。

语法声明左侧的允许规则 #

这里整理几个关键规则：

• Lambda绑定必须是单个变量：不能用λ x y → ...这种多变量缩写，必须写成嵌套的λ x → λ y → ...形式，让解析器逐个识别绑定变量。
• 自定义语法的结构要和函数参数匹配：你的自定义语法（比如swap[ x , y ] body）里的变量，必须对应到嵌套Lambda的每个绑定层级。
• 分隔符（比如逗号）只是语法糖：你可以用逗号、空格等分隔变量，但背后必须对应正确的嵌套Lambda绑定，才能保证变量作用域被正确解析。

解决你的swap示例问题 #

把多变量Lambda拆成嵌套的单变量Lambda，就能正常定义自定义语法了：

swap : {A B C : Set} → (A → B → C) → B → A → C
swap f y x = f x y
-- 用嵌套Lambda绑定两个变量，对应自定义语法里的x,y
syntax swap (λ x → λ y → body) = swap[ x , y ] body

这样你就能用swap[ x , y ] (x + y)这种简洁的语法来调用swap了，Agda会正确解析为swap (λ x y → x + y)。

参考标准库的写法 #

其实Agda标准库中的多变量构造（比如嵌套的Σ类型）也是遵循这个规则的：比如Σ[ x ∈ A ][ y ∈ B ] C，背后对应的是Σ A (λ x → Σ B (λ y → C))，本质就是嵌套的单变量Lambda绑定，和我们上面的写法逻辑一致。

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