Haskell 中的 Y 组合器

Question

是否可以在 Haskell 中编写 Y Combinator ？

看起来它会有无限递归类型。

 Y :: f -> b -> c
 where f :: (f -> b -> c)

或者什么的。即使是简单的稍微因式分解的阶乘

factMaker _ 0 = 1
factMaker fn n = n * ((fn fn) (n -1)

{- to be called as
(factMaker factMaker) 5
-}

也会失败，并显示“发生检查：无法构造无限类型：t = t -> t2 -> t1”

（Y 组合器

(define Y
    (lambda (X)
      ((lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg))))
       (lambda (procedure)
         (X (lambda (arg) ((procedure procedure) arg)))))))

在方案中看起来像这样） 或者，更简洁地称为“

(λ (f) ((λ (x) (f (λ (a) ((x x) a))))
        (λ (x) (f (λ (a) ((x x) a))))))

对于应用顺序” 对于惰性版本来说，这

(λ (f) ((λ (x) (f (x x)))
        (λ (x) (f (x x)))))

只是一个 eta 缩写。

如果您喜欢短变量名。

Answer 1

这是 haskell 中 y 组合器的非递归定义：

newtype Mu a = Mu (Mu a -> a)
y f = (\h -> h $ Mu h) (\x -> f . (\(Mu g) -> g) x $ x)

帽子提示

Answer 2

Y 组合器不能使用 Hindley-Milner 类型进行类型化，Hindley-Milner 类型是 Haskell 类型系统所基于的多态 lambda 演算。您可以通过诉诸类型系统的规则来证明这一点。

我不知道是否可以通过给 Y 组合器一个更高级别的类型来输入它。这会让我感到惊讶，但我没有证据证明这是不可能的。 （关键是为 lambda 绑定的 x 确定一种合适的多态类型。）

如果您想要在 Haskell 中使用定点运算符，您可以非常轻松地定义一个，因为在 Haskell 中，let-bound具有定点语义：

fix :: (a -> a) -> a
fix f = f (fix f)

您可以以通常的方式使用它来定义函数，甚至一些有限或无限的数据结构。

还可以使用递归类型的函数来实现定点。

如果您对定点编程感兴趣，您需要阅读 Bruce McAdam 的技术报告 至此结束。

Answer 3

Y 组合器的规范定义如下：

y = \f -> (\x -> f (x x)) (\x -> f (x x))

但由于 x x，它不会在 Haskell 中进行类型检查，因为它需要无限类型：

x :: a -> b -- x is a function
x :: a      -- x is applied to x
--------------------------------
a = a -> b  -- infinite type

如果类型系统允许此类递归类型，它会使类型检查变得不可判定（容易出现无限循环）。

但是，如果您强制 Y 组合器进行类型检查，例如通过使用 unsafeCoerce :: a -> b：

import Unsafe.Coerce

y :: (a -> a) -> a
y = \f -> (\x -> f (unsafeCoerce x x)) (\x -> f (unsafeCoerce x x))

main = putStrLn $ y ("circular reasoning works because " ++)

这是不安全的（显然）。 rampion 的答案演示了一种在 Haskell 中编写定点组合器而不使用递归的更安全方法。

Answer 4

哦

这个维基页面和
这个 Stack Overflow 答案似乎回答了我的问题。
稍后我会写更多的解释。

现在，我发现了关于 Mu 类型的一些有趣的事情。考虑 S = Mu Bool。

data S = S (S -> Bool)

如果将 S 视为一个集合，并且等号视为同构，则方程变为

S ⇋ S -> Bool ⇋ Powerset(S)

所以 S 是与其幂集同构的集合的集合！
但从康托尔的对角论证中我们知道，Powerset(S) 的基数总是严格大于 S 的基数，因此它们永远不是同构的。
我认为这就是为什么你现在可以定义一个定点运算符，尽管你不能没有一个定点运算符。

Answer 5

只是为了使 rampion 的代码更具可读性：

-- 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

其中 w 代表 omega 组合器 w = \x -> x x，y 代表 y 组合子y = \f ->瓦特。 （转发）。