Haskell中的Y Combinator

是否有可能在Haskell中編寫Y Combinator？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 = - > 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))))))

對於APPLICAT香港專業教育學院爲了而

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

這只是一個埃塔收縮離開懶惰的版本。

如果您更喜歡短變量名稱。

來源

2010-11-25 Theo Belaire

哦

this wiki page和 This Stack Overflow answer似乎回答我的問題。
我稍後會寫出更多的解釋。

現在，我發現了一些有關Mu類型的東西。考慮S =穆布爾。

data S = S (S -> Bool)

如果一個人把S作爲一組，並且等號類質同象，那麼等式變成

S ⇋ S -> Bool ⇋ Powerset(S)

所以S是一套套是同構他們冪！但是我們從Cantor的對角論證中知道Powerset（S）的基數總是嚴格大於S的基數，所以它們永遠不是同構的。我想這就是爲什麼你現在可以定義一個定點操作符，即使你不能沒有一個。

來源

2010-11-25 03:17:43

+1用於自己回答問題。 – fuz 2010-11-25 05:09:08

正如另一個答案所示，如果你想要一個定點組合器，你可以在不給出類型的情況下寫`yf = f（yf）`並且編譯器將會推斷出'（t - > t） - > t'本身。如維基百科文章所示，這是一個不同的定點組合器，並不嚴格地說是y組合器。 – ShreevatsaR 2011-05-04 15:03:09

這裏的Y型組合子的哈斯克爾非遞歸定義：

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

hat tip

來源

2011-05-04 14:44:49 rampion

的Y組合的規範定義如下：

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

但由於x x因爲需要無限類型而沒有在Haskell中輸入檢查：

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中編寫一個定點組合器。

來源

2011-05-04 15:53:37

不錯！這正是`unsafeCoerce`用於：繞過類型系統的限制。 – 2012-10-11 20:38:58

不能使用Hindley-Milner類型（Haskell類型系統基於的多態lambda表達式）來鍵入Y組合器。你可以通過訴諸類型系統的規則來證明這一點。

我不知道是否可以通過給它一個更高等級的類型鍵入Y組合。這會讓我感到驚訝，但我沒有證明這是不可能的。（關鍵是要確定適當的多態型的拉姆達結合x。）

如果你想在Haskell定點操作，可以非常方便的，因爲在Haskell定義一個，讓結合了固定翼點語義：

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

你可以用通常的方式來定義函數，甚至是一些有限或無限的數據結構。

也可以使用遞歸類型的函數來實現固定點。

如果您有興趣使用固定點進行編程，您可以閱讀Bruce McAdam的技術報告That About Wraps it Up。

來源

2011-05-04 19:29:10

Haskell中的Y Combinator

回答

相關問題