在現代Haskell中可以定義Omega combinator（λx.xx）嗎？

Question

堆棧！在現代Haskell中可以定義Omega combinator（λx.xx）嗎？我猜想，Haskell98的類型系統旨在使這樣的事情變得不可能，但現代擴展又如何呢？

Answer 1

不，但有點。這裏要欣賞的是，Haskell支持newtype聲明中的無限制遞歸。根據Haskell的語義，newtype是被定義的類型和其實現類型之間的同構。因此，例如這樣的定義：

newtype Identity a = Identity { runIdentity :: a } 

...斷言類型Identity a和a是同構的。根據定義，構造函數Identity :: a -> Identity a和觀察者runIdentity :: Identity a -> a是逆逆。

所以從svenningsson的答案借用Scott類型名稱，定義如下：

newtype Scott = Scott { apply :: Scott -> Scott } 

...斷言類型Scott同構於Scott -> Scott。所以，你，而你不能直接應用Scott本身，你可以使用同構，以獲得其對應Scott -> Scott並應用到原：

omega :: Scott -> Scott 
omega x = apply x x 

或略有更有趣：

omega' :: (Scott -> Scott) -> Scott 
omega' f = f (Scott f) 

...這是一個固定點組合類型！這一招可以適應寫在Haskell一個版本的Y組合的：（FORALL A A - > FA） -

module Fix where 

newtype Scott a = Scott { apply :: Scott a -> a } 

-- | This version of 'fix' is fundamentally the Y combinator, but using the 
-- 'Scott' type to get around Haskell's prohibition on self-application (see 
-- the expression @apply x x@, which is @x@ applied to itself). Example: 
-- 
-- >>> take 15 $ fix ([1..10]++) 
-- [1,2,3,4,5,6,7,8,9,10,1,2,3,4,5] 
fix :: (a -> a) -> a 
fix f = (\x -> f (apply x x)) (Scott (\x -> f (apply x x))) 

Answer 2

嗯，你可以定義：

{-# LANGUAGE Rank2Types #-} 

omega :: (forall a . a) -> b 
omega x = x x 

然而，這是幾乎無用的，因爲可以作爲參數傳遞的唯一價值是undefined，所以你不能把它作爲一個組合子都沒有。即使omega omega未能輸入檢查。

美中不足的是，爲了x x來進行類型檢查你有一個類型爲類型xT = t -> s並在t與T統一（這樣就可以通過x自身）。但這基本上意味着t必須是一個類型變量，並且參數必須是完全多態的，從而使該函數無用。

Answer 3

你不能在Haskell中直接表示歐米茄。有很少的類型系統可以表示自我應用，而Haskell的類型系統不是其中之一。但是你可以編碼類型化演算和模擬歐米茄和自我應用，像這樣：

data Scott = Scott { apply :: Scott -> Scott } 

omega = Scott $ \x -> apply x x 

現在你可以說apply omega omega，並得到一個非終止計算。如果你想嘗試一下在ghci中，你可能想以下Show實例

instance Show Scott where 
    show (Scott _) = "Scott" 

Answer 4

好，

omega :: a -> a 
omega x = unsafeCoerce x x 

甚至

omega :: a -> IO a 
omega x = do 
    putStrLn "Why are you doing this to me?" 
    unsafeCoerce x x 

main = omega omega 

你爲什麼做這無限期版畫」這對我？「。