Haskell实现Church数前驱函数的rigid type与无限类型报错求解

错误原因解析 #

1. pred2报错原因 #

首先明确Church新类型的定义：newtype Church = Church { runChurch :: forall a. (a -> a) -> a -> a }，这里构造器Church要求传入的函数必须是对任意类型a都生效的多态函数，这是邱奇数的核心要求：同一个邱奇数可以在任意类型场景下做迭代，比如邱奇3既可以迭代函数计算3次幂，也可以迭代函数拼接3次字符串。
而你给pred2写的签名里，参数n的类型是((a -> a) -> a -> a)，这里的a是签名开头forall a绑定的、固定的某一个类型，不是对所有a都通用的多态函数。你把这种固定了a的n传给需要全多态函数的Church构造器，自然会出现类型不匹配的报错，GHC提示的a1就是Church构造器要求的任意a，和你签名里固定的a无法统一。
修正方法很简单，给n加上forall限定，让它变成真正的邱奇数多态类型：

pred2 :: forall a. (forall b. (b -> b) -> b -> b) -> (a -> a) -> a -> a
pred2 n = runChurch $ pred1 (Church n)

这时候n是对任意b都生效的多态函数，符合Church构造器的要求，就可以正常编译了。

2. pred3报错原因 #

这个报错本质和pred2是同源的：你给pred3写的签名里n的类型还是固定了单态a的((a -> a) -> a -> a)，而邱奇数前驱的实现逻辑里，迭代过程的中间值类型和最终返回的a类型是不一样的：
你传入给n的迭代函数\g h -> h (g f)要求中间的g的类型是嵌套的函数类型，和你最终要返回的a不是同一个类型，但你签名里强制要求n的所有操作都在同一个a类型下进行，就会触发类型检查的occurs check，检测到你要构造无限递归的类型（a要包含它自己），所以直接报错。
你没写签名时GHC推导出来的类型里有多个不同的类型变量，就是因为它识别到了中间值和最终值类型不一样，但你手动给的签名强制所有类型都统一为a，自然就不匹配了。
如果要让pred3不用Church包装也能编译，同样需要给n加上高阶多态限定，并且允许中间迭代的类型和最终返回类型分离，正确的签名写法如下：

{-# LANGUAGE RankNTypes #-}
pred3 :: forall a. (forall b. (b -> b) -> b -> b) -> (a -> a) -> a -> a
pred3 n f a1 = extract (n (\g h -> h (g f)) (const a1)) where
  extract k = k id

这个写法里n是对任意b都生效的多态函数，迭代过程可以用和最终a不同的中间类型b，就不会触发无限类型错误，可以正常编译运行。

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