Haskell中Church数乘法实现报错及add1与add one差异疑问

一、mul cn cm = cn (add cm) zero的类型错误原因 #

先明确Church编码的核心类型定义：

• 自然数n的Church编码（记为CNum）类型是：(a -> a) -> a -> a，表示将函数f组合n次后应用到x上。
• 标准加法函数add的类型是：CNum -> CNum -> CNum，即接受两个Church数，返回它们的和（仍是Church数）。

你的错误实现里，cn作为Church数，它的第一个参数要求是单参数函数（类型t -> t），但add cm的结果是CNum类型（即(a->a)->a->a）——这是柯里化的双参数函数，和cn期望的参数类型不匹配，因此触发类型错误。

正确乘法实现mul cn cm = \f x -> cn (cm f) x的逻辑是：

• cm f将函数f组合cm次，得到一个单参数函数（类型a->a），完全符合cn对第一个参数的类型要求；
• cn (cm f) x将这个组合后的函数再应用cn次，等价于把f应用cn * cm次，完美匹配乘法的Church编码语义。

二、test与test2的差异原因 #

先拆解两个函数的核心逻辑：

• add1应该是后继函数succ，标准实现为succ n = \f x -> f (n f x)，类型CNum -> CNum，作用是给输入的Church数加1。
• 若add是标准实现add m n = \f x -> m f (n f x)，那么add one等价于succ：

  add one n = \f x -> one f (n f x) = \f x -> f (n f x) = succ n
  

按此逻辑，test cn = cn succ zero和test2 cn = cn (add one) zero应该完全等价——都是将后继函数应用cn次到zero上，得到cn对应的自然数。但你说test2仅对zero、one有效，大概率是你的add函数实现错误：

• 比如误把加法写成了乘法：add m n = \f x -> m (n f) x（这实际是乘法逻辑），此时add one n = \f x -> one (n f) x = n，即add one是恒等函数而非后继函数；
• 这种情况下test2 cn = cn id zero，id函数不管应用多少次到zero上结果都是zero，自然只有zero、one的测试结果看似符合预期（实际逻辑已错误）。

请检查你的add函数是否符合标准加法的Church编码逻辑：add m n = \f x -> m f (n f x)。

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