haskell - usando - ¿Por qué este código que utiliza UndecidableInstances se compila, luego genera un bucle infinito en tiempo de ejecución?

ciclo for

Question

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 desde a -> Foo y Foo -> 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 de convertFoo , 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?

Answer 1

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 directamente ConvertFoo Int String (1).
• Entonces, (1) requiere ConvertFoo Int Foo (2) y ConvertFoo Foo String (3).
• Luego, (2) requiere ConvertFoo Int Foo (ya contamos esto) y ConvertFoo Foo Foo (4).
• Entonces (3) requiere ConvertFoo Foo Foo (contado) y ConvertFoo Foo String (contado).
• Entonces (4) requiere ConvertFoo Foo Foo (contado) y ConvertFoo 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.

Answer 2

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.