online - Haskell/GHC UndecidableInstances-¿Ejemplo para verificación de tipo sin terminación?

haskell compiler online

Question

He escrito un código Haskell que necesita -XUndecidableInstances para compilar. Entiendo por qué sucede eso, hay una cierta condición que se viola y, por lo tanto, GHC grita.

Sin embargo, nunca me he encontrado con una situación en la que el verificador de tipos en realidad se cuelgue o termine en un bucle sin fin.

¿Qué aspecto tiene una definición de instancia sin terminación? ¿Puede dar un ejemplo?

Answer 1

Hay un ejemplo clásico, algo alarmante (que involucra la interacción con dependencias funcionales) en este documento de 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

Necesitamos que mul x [y] tenga el mismo tipo que y , entonces, tomando x :: x e y :: y , necesitamos

instance Mul x [y] y

Que, según la instancia dada, podemos tener. Por supuesto, debemos tomar y ~ [z] para algunos z modo que

instance Mul x y z

es decir

instance Mul x [z] z

y estamos en un bucle.

Es preocupante, porque esa instancia de Mul parece que su recursión está reduciéndose estructuralmente, a diferencia de la instancia claramente patológica en la respuesta de Petr. Sin embargo, hace un circuito de GHC (con el umbral de aburrimiento pateando para evitar colgar).

El problema, como estoy seguro que mencioné en algún lugar en algún momento, es que la identificación y ~ [z] se realiza a pesar del hecho de que z depende funcionalmente de y . Si usamos una notación funcional para la dependencia funcional, podríamos ver que la restricción dice y ~ Mul x [y] y rechazar la sustitución como una violación de la verificación de ocurrencia.

Intrigado, pensé que le daría un giro a esto,

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

Con UndecidableInstances habilitado, se tarda bastante tiempo en que el ciclo se agote. Con UndecidableInstances desactivado, la instancia aún se acepta y el buscador de tipos aún se repite, pero el corte se produce mucho más rápidamente.

Así que ... divertido viejo mundo.

Answer 2

Por ejemplo:

{-# LANGUAGE UndecidableInstances #-}

class C a where
    f :: a -> a

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

g x = x + f [x]

Qué sucede: al escribir f [x] el compilador debe asegurarse de que x :: C [a] para algunos a . La declaración de instancia dice que x puede ser de tipo C [a] solo si también es de tipo C [[a]] . Así que el compilador necesita asegurarse de que x :: C [[a]] , etc. y quede atrapado en un bucle infinito.

Consulte también ¿Puede usar Pragma de Undecidable Instances localmente tener consecuencias globales en la finalización de la compilación?