Haskell/GHC UndecidableInstances - Beispiel für nicht abschließende Typprüfung?

Question

Ich habe einen Haskell-Code geschrieben, der -XUndecidableInstances kompilieren muss. Ich verstehe, warum das passiert, dass es eine bestimmte Bedingung gibt, die verletzt wird und deshalb schreit GHC.

Allerdings bin ich nie auf eine Situation gestoßen, in der der Typ-Checker tatsächlich in einer Endlosschleife hängen oder enden würde.

Wie sieht eine nicht abschließende Instanzdefinition aus - können Sie ein Beispiel geben?

Answer 1

Zum Beispiel:

{-# LANGUAGE UndecidableInstances #-} 

class C a where 
    f :: a -> a 

instance C [[a]] => C [a] where 
    f = id 

g x = x + f [x] 

Was geschieht: Wenn f [x] Eingabe der Compiler muss, dass x :: C [a] für einige a gewährleisten. Die Instanzdeklaration besagt, dass x nur dann vom Typ C [a] sein kann, wenn sie auch vom Typ C [[a]] ist. Also muss der Compiler sicherstellen, dass x :: C [[a]] usw. und in einer Endlosschleife gefangen wird.

Siehe auch Can using UndecidableInstances pragma locally have global consequences on compilation termination?

Answer 2

Es ist eine klassische, etwas alarmierend Beispiel (die einen Dialog mit funktionalen Abhängigkeiten) in this paper from HQ:

class Mul a b c | a b -> c where 
    mul :: a -> b -> c 
instance Mul a b c => Mul a [b] [c] where 
    mul a = map (mul a) 

f b x y = if b then mul x [y] else y 

Wir mul x [y] müssen den gleichen Typ wie y haben, also unter x :: x und y :: y, wir brauchen

instance Mul x [y] y 

whi ch, je nach gegebenem Beispiel, können wir haben. Natürlich müssen wir y ~ [z] für einige z so nehmen, dass

instance Mul x y z 

heißt

instance Mul x [z] z 

und wir in einer Schleife sind.

Es ist beunruhigend, denn das Mul Beispiel aussieht seine Rekursion strukturell ist , im Gegensatz zu dem deutlich pathologischen Beispiel in Petr Antwort zu reduzieren. Aber es macht GHC-Schleife (mit der Langeweile Schwelle, um zu vermeiden, hängen).

Das Problem, wie ich bin sicher, dass ich irgendwo irgendwann erwähnt habe, ist, dass die Identifizierung y ~ [z] trotz der Tatsache Gebrauch gemacht wird, dass z funktionell auf y abhängt. Wenn wir eine funktionale Notation für die funktionale Abhängigkeit verwenden, sehen wir möglicherweise, dass die Einschränkung y ~ Mul x [y] lautet und die Substitution als Verletzung der Vorkommnisprüfung zurückweist.

Neugierig geworden, dachte ich, ich würde dies einen Wirbel geben,

class Mul' a b where 
    type MulT a b 
    mul' :: a -> b -> MulT a b 

instance Mul' a b => Mul' a [b] where 
    type MulT a [b] = [MulT a b] 
    mul' a = map (mul' a) 

g b x y = if b then mul' x [y] else y 

Mit UndecidableInstances aktiviert ist, dauert es eine ganze Weile für die Schleife zu Zeit. Wenn UndecidableInstances deaktiviert ist, wird die Instanz weiterhin akzeptiert, und der Typchecker führt immer noch eine Schleife aus, aber die Abschaltung erfolgt viel schneller.

Also ... lustige alte Welt.