Можно ли определить комбинатор Omega (λx.xx) в современном Haskell?

Question

Стек! Можно ли определить комбинатор Omega (λx.xx) в современном Haskell? Я полагаю, система типа Haskell98 предназначена для того, чтобы сделать такие вещи невозможными, но как насчет современных расширений?

Answer 1

Нет, но вроде. Здесь стоит отметить, что Haskell поддерживает неограниченную рекурсию в объявлениях newtype. По семантике Haskell, newtype является изоморфизмом между определяемым типом и его типом реализации. Так, например, такое определение:

newtype Identity a = Identity { runIdentity :: a } 

... утверждает, что типы Identity a и a изоморфны. Конструктор Identity :: a -> Identity a и наблюдатель runIdentity :: Identity a -> a являются обратными, по определению.

Так позаимствовав имя Scott типа от ответа svenningsson, в следующее определение:

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) 

... который является комбинатором фиксированных точек! Этот прием может быть адаптирован для написания версии Y Combinator в Haskell: (. ForAll а а -> фа) -

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 к typecheck вы должны ввести x с типом T = 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 

, которые на неопределенный срок печатает «Почему вы это делаете это мне? ».