Y组合在Haskell

是否有可能在Haskell中编写Y Combinator ?

它似乎会有一个无限的recursiontypes。

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

“发生检查:不能构造无限types: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) ((xx) a)))) (λ (x) (f (λ (a) ((xx) a)))))) 

对于应用程序和

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

对于懒惰的版本,这仅仅是一个eta收缩。

如果你喜欢短的variables名称。

下面是haskell中的y-combinator的非recursion定义:

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

帽子提示

Y组合器不能使用Hindley-Milnertypes,Haskelltypes系统基于的多态lambdaexpression式来input。 你可以通过诉诸types系统的规则来certificate这一点。

我不知道是否可以通过给它一个更高级的types键入Y组合。 这会让我感到惊讶,但是我没有证据certificate这是不可能的。 (关键是为lambda-bound x确定一个适当的多态types。)

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

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

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

也可以使用recursiontypes的函数来实现固定点。

如果你对固定点编程感兴趣,你可以阅读Bruce McAdam 关于包装的技术报告。

这个维基页面和这个堆栈溢出的答案似乎回答我的问题。
我稍后会写更多的解释。

现在,我发现了一些有关Mutypes的东西。 考虑S =穆布尔。

 data S = S (S -> Bool) 

如果把S看作一个集合,把等号当作同构,那么方程就变成了

 S ⇋ S -> Bool ⇋ Powerset(S) 

所以S是与他们的同类同构的集合! 但是我们从Cantor的对angular论证中知道Powerset(S)的基数总是严格大于S的基数,所以它们决不是同构的。 我想这就是为什么你现在可以定义一个定点操作符,即使你不能没有一个。

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

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

但是由于xx ,它没有在Haskell中检查types,因为它需要一个无限的types:

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

如果types系统允许这样的recursiontypes,它将使types检查不可判定(容易出现无限循环)。

但是,如果你强迫它检查,例如通过使用unsafeCoerce :: a -> b

 import Unsafe.Coerce y :: (a -> a) -> a y = \f -> (\x -> f (unsafeCoerce xx)) (\x -> f (unsafeCoerce xx)) main = putStrLn $ y ("circular reasoning works because " ++) 

这是不安全的(显然)。 rampion的答案演示了一种更安全的方法来在Haskell中编写一个定点组合器,而不使用recursion。