50

是否可以在 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 收缩。

如果您更喜欢短变量名。

4

5 回答 5

57

这是 haskell 中 y-combinator 的非递归定义：

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

帽尖

于 2011-05-04T14:44:49.357 回答
47

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

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

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

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

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

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

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

于 2011-05-04T19:29:10.643 回答
30

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

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

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

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 中编写定点组合器而不使用递归的更安全方法。

于 2011-05-04T15:53:37.633 回答
24

哦

这个 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 的基数，所以它们绝不是同构的。我认为这就是为什么你现在可以定义一个定点运算符，即使你不能没有一个。

于 2010-11-25T03:17:43.833 回答
1

只是为了让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 -> w . (f w)。

于 2020-04-29T16:20:51.737 回答