Est-il possible de définir le combinateur Omega (λx.xx) dans Haskell moderne?

Question

Pile! Est-il possible de définir le combinateur Omega (λx.xx) dans Haskell moderne? Je suppose que le système de types de Haskell98 est conçu pour rendre impossible ce genre de choses, mais qu'en est-il des extensions modernes?

Answer 1

Non, mais en quelque sorte. La chose à apprécier ici est que Haskell prend en charge la récursivité sans restriction dans les déclarations newtype. Par la sémantique de Haskell, un newtype est un isomorphisme entre le type en cours de définition et son type d'implémentation. Ainsi, par exemple cette définition:

newtype Identity a = Identity { runIdentity :: a } 

... affirme que les types Identity a et a sont isomorphes. Le constructeur Identity :: a -> Identity a et l'observateur runIdentity :: Identity a -> a sont inverses, par définition.

Ainsi, le nom d'emprunt de type Scott de la réponse de Svenningsson, la définition suivante:

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

... affirme que le type Scott est isomorphe à Scott -> Scott.Alors vous pendant que vous ne pouvez pas appliquer une Scott à lui-même directement, vous pouvez utiliser pour obtenir l'isomorphisme son homologue Scott -> Scott et l'appliquer à l'original:

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

Ou un peu plus intéressant:

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

... qui est un type de combinateur de point fixe! Cette astuce peut être adapté pour écrire une version du combinateur Y en Haskell: (. 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

Eh bien, vous pouvez définir:

{-# LANGUAGE Rank2Types #-} 

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

mais cela est à peu près inutile, parce que la seule valeur qui peut être passé comme argument est undefined, de sorte que vous ne pouvez pas l'utiliser comme un combinateur du tout. Même omega omega ne parvient pas à taper vérifier.

Le hic est que pour x x vous typecheck auriez à taper x avec un type T = t -> s et où t unifie avec T (pour que vous puissiez passer x à lui-même). Mais cela signifie essentiellement que t doit être une variable de type et l'argument doit être entièrement polymorphe, rendant la fonction inutile.

Answer 3

Vous ne pouvez pas représenter omega directement dans Haskell. Il y a très peu de systèmes de types qui peuvent représenter des auto-applications et le système de types de Haskell n'en fait pas partie. Mais vous pouvez coder le calcul typées lambda et simuler oméga et de l'application de l'auto comme ceci:

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

omega = Scott $ \x -> apply x x 

Maintenant, vous pouvez dire apply omega omega et obtenir un calcul non-terminaison. Si vous voulez l'essayer dans GHCi, vous voulez probablement les éléments suivants Show exemple

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

Answer 4

Eh bien,

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

Ou encore

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

main = omega omega 

qui indéfiniment imprimés « Pourquoi faites-vous cela pour moi?".