Y Combinator在Haskell中的应用

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

在scheme中)

或者更简洁地说

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

对于应用次序（Applicative Order）

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

对于懒惰的版本，这只是eta压缩的一步之遥。

如果你喜欢使用短变量名。

- Theo Belaire

Answer 1

以下是Haskell中Y组合子的非递归定义：

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

致谢

- rampion

---

我已经发布了一个答案以使这些代码更易读。答案链接 如果有帮助，请给我投票。非常感谢。 - qimokao

Answer 2

使用Hindley-Milner类型（即Haskell类型系统的基础，一种多态λ演算）无法对Y组合子进行类型推导。可以通过类型系统规则证明这一点。

我不知道是否可能通过给Y组合子赋予更高秩的类型来实现类型推导。尽管我没有证明它不可能，但这仍然会让我感到惊讶。（关键是找到一个适当的多态类型来绑定λ变量x。）

如果你想在Haskell中实现固定点运算符，很容易定义一个，因为在Haskell中，let绑定具有固定点语义：

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

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

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

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

- Norman Ramsey

---

无法使用更高级别的类型输入Y组合子 - 系统F是强规范化的。 - Philip JF

另一方面，使用递归类型键入y组合子很容易。 - Philip JF

Answer 3

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

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

但是在 Haskell 中无法进行类型检查，因为涉及到 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中编写固定点组合器而不使用递归的更安全的方法。

- Joey Adams

---

好的！这正是unsafeCoerce的用途：绕过类型系统的限制。 - Dan Burton

尽管这句话的语法是正确的，但由于“x x”的存在，它在Haskell中无法通过类型检查。该语句具有矛盾性。事实上，类型理论的发明基本上就是为了禁止自我应用。 - Luis Casillas

Answer 4

哦

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

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

data S = S (S -> Bool)

如果将S看作一个集合，等号视为同构，则该方程变为

S ⇋ S -> Bool ⇋ Powerset(S)

S集合是指那些与它们的幂集同构的集合！但是根据康托尔对角线论证，幂集(Powerset)的基数总是严格大于S的基数，因此它们永远不会同构。我认为这就是为什么现在可以定义一个固定点算子的原因，即使没有一个固定点算子也是不行的。

- Theo Belaire

---

正如其他答案所示，如果您想要一个固定点组合子，只需编写 y f = f (y f) 而不给出类型，编译器将自动推断类型 (t -> t) -> t。这是一个不同的固定点组合子，严格来说不是 y 组合子，正如维基百科文章所示。 - ShreevatsaR

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 -> w . (f w)。

- qimokao