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-combinator 的非递归定义：

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

hat tip

Answer 2

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

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

如果你想在 Haskell 中定义一个定点运算符，你可以很容易地定义一个，因为在 Haskell 中，let-binding 具有定点语义：

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

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

也可以在递归类型上使用函数来实现定点。

如果您对定点编程感兴趣，可以阅读 Bruce McAdam 的技术报告That About Wraps it Up。

Answer 3

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

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

但由于x x，它不会在 Haskell 中键入 check，因为它需要无限类型：

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's answer 演示了一种在 Haskell 中编写定点组合器而不使用递归的更安全方法。

Answer 4

哦

this wiki page 和 This Stack Overflow answer 似乎回答了我的问题。
稍后我会写更多的解释。

现在，我发现了关于那个 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 代表欧米茄组合器w = \x -> x x，y 代表y 组合器y = \f -> w . (f w)。