Haskell中SK组合子构成的s k k函数的类型与定义推导

SKK 组合子运算逻辑推导 #

我们先从最直观的表达式展开入手，不用先纠结类型：
首先明确两个组合子的定义：

s f g x = f x (g x)
k x y = x

我们直接把参数代入 s k k 的调用场景，给它补一个最后传入的参数 x：
s k k x = k x (k x)
此时看等式右边的 k x (k x)，完全符合k的调用规则：接收两个参数，返回第一个参数。这里第一个参数是x，第二个参数是(k x)，所以直接返回x。
也就是说 s k k x = x，这就是标准的恒等函数，自然类型就是 t -> t。

分步类型推导（新手友好版） #

我们再一步步对应类型签名的匹配逻辑，所有类型变量名只是占位符，匹配时只要对应关系一致即可重命名：

已知类型签名 #

s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3
k :: p1 -> p2 -> p1

S的类型可以拆解为：接收3个参数，分别是

1. 类型为 t1 -> t2 -> t3 的函数f
2. 类型为 t1 -> t2 的函数g
3. 类型为 t1 的参数x
   最终返回类型为 t3 的结果。

第一步：推导 s k 的类型 #

现在给S传入第一个参数k，需要让k的类型和S第一个参数的类型 t1 -> t2 -> t3 完全匹配：

• k的第一个参数类型 p1 = t1
• k的第二个参数类型 p2 = t2
• k的返回值类型 p1 = t3

把匹配关系代入S剩下的参数类型，S传完第一个参数后，剩下的类型就是「第二个参数的类型 -> 传完x后的返回类型」，也就是 (t1 -> t2) -> (t1 -> t3)，替换后得到：
(p1 -> p2) -> p1 -> p1
和你在GHCi查到的 (t3 -> t2) -> t3 -> t3 完全一致，只是类型变量重命名了而已。

第二步：推导 s k k 的类型 #

现在给s k传入第二个参数k，我们给这个k的类型变量换名避免冲突：k :: p3 -> p4 -> p3
需要让这个k的类型和s k要求的第一个参数类型 p1 -> p2 匹配：
因为柯里化特性，p3 -> p4 -> p3 等价于 p3 -> (p4 -> p3)，所以匹配关系为：

• p1 = p3
• p2 = p4 -> p3

把匹配关系代入s k传完参数后的返回类型 p1 -> p1，替换后得到：
p3 -> p3
也就是GHCi给出的 t -> t，和我们之前表达式推导的结论一致。

组合子通用理解方法 #

• 优先做表达式展开：把组合子的参数逐个代入定义，先明确运算逻辑，再看类型会更容易理解
• 类型推导做对齐：把传入函数的类型和外层函数要求的参数类型逐个对应，相同类型变量替换为同一个类型，最终剩余的就是组合后的类型

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