haskell - usando - ¿Por qué este código que utiliza UndecidableInstances se compila, luego genera un bucle infinito en tiempo de ejecución?
ciclo for (2)
Cuando escribí un código usando UndecidableInstances
antes, me topé con algo que me pareció muy extraño. Logré crear involuntariamente un código que comprueba cuando creía que no debía:
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE UndecidableInstances #-}
data Foo = Foo
class ConvertFoo a b where
convertFoo :: a -> b
instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
convertFoo = convertFoo . (convertFoo :: a -> Foo)
evil :: Int -> String
evil = convertFoo
Específicamente, la función convertFoo convertFoo
una comprobación cuando se le da una entrada para producir cualquier salida, como lo demuestra la función evil
. Al principio, pensé que tal vez logré implementar unsafeCoerce
accidentalmente, pero eso no es del todo cierto: en realidad, intentar llamar a mi función convertFoo
(haciendo algo como evil 3
, por ejemplo) simplemente entra en un bucle infinito.
Entiendo lo que está pasando en un sentido vago. Mi comprensión del problema es algo como esto:
- La instancia de
ConvertFoo
que he definido funciona en cualquier entrada y salida,b
, solo limitada por las dos restricciones adicionales de que las funciones de conversión deben existir desdea -> Foo
yFoo -> b
. - De alguna manera, esa definición puede coincidir con cualquier tipo de entrada y salida, por lo que parece que la llamada a
convertFoo :: a -> Foo
está escogiendo la definición misma deconvertFoo
, ya que es la única disponible, de todos modos. - Dado que
convertFoo
llama a sí mismo infinitamente, la función entra en un bucle infinito que nunca termina. - Dado que
convertFoo
nunca termina, el tipo de esa definición es la parte inferior, por lo que técnicamente ninguno de los tipos se viola, y el programa se comprueba.
Ahora, incluso si la comprensión anterior es correcta, todavía estoy confundido acerca de por qué todo el programa se comprueba. Específicamente, esperaría que las restricciones de ConvertFoo a Foo
y ConvertFoo Foo b
falle, dado que no existen tales instancias.
Entiendo (al menos fuzzmente) que las restricciones no importan al elegir una instancia: la instancia se elige basándose únicamente en el encabezado de la instancia, luego se verifican las restricciones, por lo que puedo ver que esas restricciones pueden resolverse bien debido a mi ConvertFoo ab
instancia ConvertFoo ab
, que es tan permisiva como puede ser. Sin embargo, eso requeriría que se resolviera el mismo conjunto de restricciones, lo que creo que pondría el buscador de tipos en un bucle infinito, haciendo que GHC se cuelgue en la compilación o me dé un error de desbordamiento de pila (el último de los cuales he visto antes de).
Claramente, sin embargo, el typechecker no hace un bucle, porque felizmente llega al fondo y compila felizmente mi código. ¿Por qué? ¿Cómo se satisface el contexto de la instancia en este ejemplo particular? ¿Por qué esto no me da un error de tipo o produce un bucle de comprobación de tipo?
Así es como proceso mentalmente estos casos:
class ConvertFoo a b where convertFoo :: a -> b
instance (ConvertFoo a Foo, ConvertFoo Foo b) => ConvertFoo a b where
convertFoo = ...
evil :: Int -> String
evil = convertFoo
Primero, comenzamos calculando el conjunto de instancias requeridas.
-
evil
requiere directamenteConvertFoo Int String
(1). - Entonces, (1) requiere
ConvertFoo Int Foo
(2) yConvertFoo Foo String
(3). - Luego, (2) requiere
ConvertFoo Int Foo
(ya contamos esto) yConvertFoo Foo Foo
(4). - Entonces (3) requiere
ConvertFoo Foo Foo
(contado) yConvertFoo Foo String
(contado). - Entonces (4) requiere
ConvertFoo Foo Foo
(contado) yConvertFoo Foo Foo
(contado).
Por lo tanto, llegamos a un punto fijo, que es un conjunto finito de instancias requeridas. El compilador no tiene problemas con la computación que se establece en un tiempo finito: simplemente aplique las definiciones de instancia hasta que no se necesiten más restricciones.
Luego, procedemos a proporcionar el código para esas instancias. Aquí está.
convertFoo_1 :: Int -> String
convertFoo_1 = convertFoo_3 . convertFoo_2
convertFoo_2 :: Int -> Foo
convertFoo_2 = convertFoo_4 . convertFoo_2
convertFoo_3 :: Foo -> String
convertFoo_3 = convertFoo_3 . convertFoo_4
convertFoo_4 :: Foo -> Foo
convertFoo_4 = convertFoo_4 . convertFoo_4
Obtenemos un montón de definiciones de instancias recursivas entre sí. Estos, en este caso, se repetirán en tiempo de ejecución, pero no hay razón para rechazarlos en tiempo de compilación.
Estoy totalmente de acuerdo en que esta es una gran pregunta. Habla de cómo nuestras intuiciones sobre las clases de tipos difieren de la realidad.
Clase de sorpresa
Para ver lo que está pasando aquí, vamos a aumentar las apuestas en la firma de tipo para el evil
:
data X
class Convert a b where
convert :: a -> b
instance (Convert a X, Convert X b) => Convert a b where
convert = convert . (convert :: a -> X)
evil :: a -> b
evil = convert
Claramente, la instancia de Covert ab
se está eligiendo ya que solo hay una instancia de esta clase. El typechecker está pensando algo como esto:
-
Convert a X
es verdadero si ...-
Convert a X
es verdadero [verdadero por supuesto] - y
Convert XX
es cierto-
Convert XX
es verdadero si ...-
Convert XX
es verdadero [verdadero por supuesto] -
Convert XX
es verdadero [verdadero por supuesto]
-
-
-
-
Convert X b
es verdadero si ...-
Convert XX
es verdadero [verdadero desde arriba] - y
Convert X b
es verdadero [verdadero por supuesto]
-
El typechecker nos ha sorprendido. No esperamos que Convert XX
sea verdadero, ya que no hemos definido nada igual. Pero (Convert XX, Convert XX) => Convert XX
es un tipo de tautología: es verdad automáticamente y es verdad sin importar qué métodos estén definidos en la clase.
Esto podría no coincidir con nuestro modelo mental de typeclasses. Esperamos que el compilador gawk en este punto y se queje de que Convert XX
no puede ser cierto porque no hemos definido ninguna instancia para él. Esperamos que el compilador esté en el Convert XX
, que busque otro lugar para caminar hacia donde Convert XX
sea verdadero, y que se rinda porque no hay otro lugar donde eso sea cierto. ¡Pero el compilador es capaz de repetir! Recurse, loop, y ser Turing-completo.
Bendecimos al verificador de tipos con esta capacidad y lo hicimos con UndecidableInstances
. Cuando la documentación indica que es posible enviar el compilador a un bucle, es fácil suponer lo peor y asumimos que los bucles malos son siempre bucles infinitos. Pero aquí hemos demostrado un bucle aún más letal, un bucle que termina , excepto de una manera sorprendente.
(Esto se demuestra aún más crudamente en el comentario de Daniel:
class Loop a where
loop :: a
instance Loop a => Loop a where
loop = loop
.)
Los peligros de la indecidibilidad.
Este es el tipo exacto de situación que permite UndecidableInstances
. Si desactivamos esa extensión y activamos FlexibleContexts
(una extensión inofensiva que es solo de naturaleza sintáctica), recibimos una advertencia sobre una violación de una de las condiciones de Paterson :
...
Constraint is no smaller than the instance head
in the constraint: Convert a X
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’
...
Constraint is no smaller than the instance head
in the constraint: Convert X b
(Use UndecidableInstances to permit this)
In the instance declaration for ‘Convert a b’
"No más pequeño que el encabezado de la instancia", aunque podemos reescribirlo mentalmente como "es posible que esta instancia se use para probar una afirmación de sí misma y causarle mucha angustia, rechinar y escribir". Las condiciones de Paterson juntas evitan los bucles en la resolución de la instancia. Nuestra violación aquí demuestra por qué son necesarios, y probablemente podemos consultar algún documento para ver por qué son suficientes.
Tocando fondo
En cuanto a por qué el programa en tiempo de ejecución bucles infinitos: hay una respuesta aburrida, donde el evil :: a -> b
no puede sino un bucle infinito o lanzar una excepción o generalmente tocar fondo porque confiamos en el buscador de tipos de Haskell y no hay valor que pueda habitar a -> b
excepto la parte inferior.
Una respuesta más interesante es que, dado que Convert XX
es tautológicamente cierto, su definición de instancia es este bucle infinito
convertXX :: X -> X
convertXX = convertXX . convertXX
Podemos expandir de manera similar la definición de instancia de Convert AB
.
convertAB :: A -> B
convertAB =
convertXB . convertAX
where
convertAX = convertXX . convertAX
convertXX = convertXX . convertXX
convertXB = convertXB . convertXX
Este comportamiento sorprendente, y cómo se supone que la resolución de instancia restringida (por defecto sin extensiones) es para evitar estos comportamientos, tal vez se pueda tomar como una buena razón por la cual el sistema de clase de tipos de Haskell aún no ha adoptado una amplia adopción. A pesar de su impresionante popularidad y poder, hay rincones extraños (ya sea en la documentación, en los mensajes de error o en la sintaxis o incluso en su lógica subyacente) que parecen particularmente mal ajustados a cómo pensamos los humanos acerca de las abstracciones a nivel de tipo.