在Haskell中定义Y组合子
在Haskell中定义Y组合子
这篇文章的创作动机是：看到了这个问题：Y Combinator in Haskell. 我之前遇到这个问题，没有思考过解决办法。而这个问题给出很多好的解决方法，于是对于其中具有代表性的方法进行了解读。
本文分为四个部分：给出预备知识；定义问题；介绍解法；进行拓展。所有的lambda表达式都是用Haskell语法书写的。有些地方为了方便，表达式的书写风格不太好，但是保证读者可以看懂。
阅读本文之前推荐先阅读推导Y组合子。
预备知识
omega组合子
-
定义：
w = \f -> f f -
性质：
w w = w w
不动点
- 定义：如果
f g = g，则称g是f的不动点。这里的f是一个函数，而g可以是一个函数，也可以是一个值。 - 不动点组合子：Fixed-point combinator（不动点组合子）是具有不动点性质的函数：
forall f, fix f = f (fix f)。
Y组合子
-
定义：
Y = \f -> (\x -> f (x x)) (\x -> f (x x))；这个定义是Haskell Curry给出的，所以在下文中称为Y组合子的curry定义。 -
性质：
Y = \f -> w (f . w)- 不动点性质：
forall f, f (Y f) = Y f。
-
Y组合子和不动点组合子
fix的关系：Y组合子的curry定义是一个纯lambda calculus的函数，而且这个函数满足不动点性质。因此，Y组合子的curry定义（这个纯lambda calculus的函数）是不动点组合子fix的一种非递归的实现方案。
利用Y组合子定义递归函数
对于一般的一阶递归函数，即定义中只因引用自身导致递归的函数，它们具有形式f = ...f...。在这种情况下，可以借助Y组合子在untyped lambda calculus下给出一个纯lambda的定义：
-
递归函数
f = ...f... -
提出非递归函数：
f' = \f -> ...f...，满足f' f = f -
借助Y组合子，定义递归函数：
f = Y f'
比如阶乘函数fac：
cond True x y = x
cond False x y = y
w = \f -> f f
y = \f -> w (f . w)
fac' = \f -> \x -> cond (x==0) 1 (x * (f (x-1)))
fac = y fac'
问题
我们试图把上一节阶乘函数的定义翻译成Haskell代码，但是发现Y组合子在Haskell中无法直接定义。
问题描述
手动确定每个函数的类型之后，上一节阶乘函数的定义变成了这样的Haskell代码：
cond :: Bool -> a -> a -> a
cond True x y = x
cond False x y = y
y :: (a -> a) -> a
y = \f -> (\x -> f (x x)) (\x -> f (x x))
fac' :: (Num a, Eq a) => (a -> a) -> a -> a
fac' = \f -> \x -> cond (x == 0) 1 (x * f (x - 1))
fac :: (Num a, Eq a) => a -> a
fac = y fac'
然而上面的这段代码会报错：Occurs check: cannot construct the infinite type。这是因为Haskell不支持递归类型，所以Y组合子（函数y）在Haskell里面无法定义。
omega组合子和Y组合子的类型的递归性
omega组合子和Y组合子（包括上一篇文章提到的满足h h = fac的h函数）不能在Haskell中直接定义，是因为他们具有递归类型。
对于omega组合子，记w w的类型为a，w的类型为b，那么在w w中第二个w的类型为b，所以第一个w的类型为b -> a，那么w的类型b满足b = b -> a，这显然是一个递归的类型。
对于Y组合子，根据性质Y f = f (Y f)，知道等式两边的类型都是a，f的类型是a -> a，所以Y组合子的类型是(a -> a) -> a。但是Y组合子内部实现中带有递归，比如在Y组合子的curry定义中，Y = \f -> (\x -> f (x x)) (\x -> f (x x))，x的类型是递归的，导致这个式子不能在Haskell中通过类型检查，所以上文的代码会报错。
解决方法
本节基于Y Combinator in Haskell的回答，给出了一些解决方案：
- 容忍递归类型
- 类型的递归 -> 组合子的递归定义
- 类型的递归 -> 构造支持描述这种递归的类型
后面的两种方法是我们讲述的重点：这两种方法本质都是把两种组合子类型上的递归性转化为其他方面的递归性，而这种其他方面的递归型可以用Haskell允许的语法表示。
容忍递归类型
import Unsafe.Coerce
y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))
简单但有效的办法。由于理论性并不很强，在此就不赘述了。
构造递归的组合子：不动点组合子
通过递归地定义不动点组合子fix，来完成递归函数的定义。
考虑到我们定义Y组合子，只是为了用Y组合子的不动点性质，不妨直接定义满足不动点性质的函数fix：
fix :: (a -> a) -> a
fix f = f (fix f)
fac :: (Num a, Eq a) => a -> a
fac = fix fac'
这种解法的好处在于，没有思考成本，直接使用不动点性质的原始公式（f (Y f) = Y f），就定义出来了能用的东西。但因为原始公式中自身蕴含的递归性，这里的fix不是用纯的lambda expression定义的，而是用pattern match递归定义的。
（在这种定义方案下，阶乘函数fac的正确性证明留给读者。）
构造递归类型：Mu
这种解法通过定义一个递归的类型Mu，使omega组合子和Y组合子能够在Haskell里有一个类型，来完成递归函数的定义。如下：
newtype Mu a = Mu (Mu a -> a)
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)
这段代码虽然一看就知道是从y = \f -> w (f . w)过来的，但是可读性实在是太差了。这促使我（花了亿点点时间）把这段代码化简成了这样：
-- Mu :: (Mu a -> a) -> Mu a
newtype Mu a = Mu (Mu a -> a)
w :: (Mu a -> a) -> a
w h = h (Mu h)
y :: (a -> a) -> a
y f = w (\(Mu x) -> f (w x))
-- y f = f . y f
把omega从y拎出来，把所有函数的类型写明，极大提升了可读性。
证明这段代码有效：证明y f = f . y f
y f
= w (\(Mu x) -> f (w x)) -- apply y
= (\(Mu x) -> f (w x)) (Mu (\(Mu x) -> f (w x))) -- apply w
= f (w (\(Mu x) -> f (w x))) -- apply (\(Mu x) -> f (w x))
= f (y f) -- y f = w (\(Mu x) -> f (w x))
= f . y f
（在这种定义方案下，阶乘函数的正确性证明留给读者。）
思考
读者此时一定非常好奇：Mu是怎么想出来的？与其像w和Y的引入一样，再次通过一个实际问题引入Mu，我们此时从一个更宏观的视角看这个问题。
无论是使用omega组合子，Y组合子和Mu类型，都是对递归的模式进行了总结和抽象，并形成高阶的函数/模式进行表示。这一类函数被统一在recursion-schemes这个包里，Haskell包的作者是Edward Kmett。GoogleEd Kmett recursion-scheme可以获得更多相关资料，包括Awesome Recursion Schemes ，recursion-schemes这些。
参考
The implementation of functional programming languages