Haskell中的Y Combinator

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

这只是懒惰版本的缩减.

如果您更喜欢短变量名称.

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)

帽子小费

Answer 2

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

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

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

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

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

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

如果你对使用固定点编程感兴趣,你想阅读Bruce McAdam的技术报告"关于包装它".

Answer 3

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中编写fixpoint组合器的更安全的方法.

Answer 4

哦

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

现在,我发现了一些有趣的Mu类型.考虑S = Mu Bool.

data S = S (S -> Bool)

如果将S视为一组并将等于符号视为同构,则等式变为

S ? S -> Bool ? Powerset(S)

所以S是与其powerset同构的一组集合!但是我们从康托尔的对角论证中得知,Powerset(S)的基数总是严格地大于S的基数,因此它们从不是同构的.我认为这就是为什么你现在可以定义一个固定点运算符,即使你不能没有一个.