haskell typechecking type-theory

¿Hay firmas de tipo que Haskell no puede verificar?



typechecking type-theory (2)

Este documento establece que la inferencia de tipo (denominada "tipificación" en el documento) en el Sistema F es indecidible. Lo que nunca he oído mencionar en otro lugar es el segundo resultado del documento, a saber, que la "comprobación de tipo" en F también es indecidible. Aquí, la pregunta de "comprobación de tipo" significa: dado un término t , tipo T y entorno de escritura A , ¿es el juicio A ⊢ t : T derivable? Me sorprende que esta pregunta sea indecidible (y que sea equivalente a la tipificación) porque me parece intuitivamente que debería ser una pregunta más fácil de responder.

Pero en cualquier caso, dado que Haskell se basa en el Sistema F (o F-omega, incluso), el resultado sobre la verificación de tipos parece sugerir que hay un término Haskell t y un tipo T tal que el compilador no podría decidir si t :: T es válido Si ese es el caso, tengo curiosidad sobre qué tipo de término y tipo son ... si no es así, ¿qué estoy entendiendo mal?

Presumiblemente, comprender el documento llevaría a una respuesta constructiva, pero estoy un poco fuera de mi alcance :)

La verificación de tipos se puede hacer decidible al enriquecer la sintaxis de manera apropiada. Por ejemplo, en el documento, tenemos lambdas escritas como /x -> e ; para teclear esto, debes adivinar el tipo de x . Sin embargo, con una sintaxis adecuadamente enriquecida, esto puede escribirse como /x :: t -> e lugar, lo que elimina las conjeturas del proceso. De manera similar, en el documento, permiten que las lambdas a nivel de tipo sean implícitas; es decir, si e :: t , entonces también e :: forall a. t e :: forall a. t Para realizar la verificación de tipos, debe adivinar cuándo y cuántos debe agregar y cuándo eliminarlos. Como antes, puede hacer esto más determinista agregando sintaxis: agregamos dos nuevas formas de expresión //a. e //a. e y e [t] y dos nuevas reglas de escritura que dicen si e :: t , entonces //a. e :: forall a. t //a. e :: forall a. t //a. e :: forall a. t , y si e :: forall a. t e :: forall a. t , entonces e [t''] :: t [t'' / a] (donde los corchetes en t [t'' / a] son corchetes de sustitución). Luego, la sintaxis nos dice cuándo y cuántos foralls agregar, y cuándo eliminarlos también.

Entonces, la pregunta es: ¿podemos pasar de Haskell a términos del Sistema F suficientemente anotados? Y la respuesta es sí, gracias a algunas restricciones críticas puestas por el sistema de tipo Haskell. Lo más crítico es que todos los tipos son de rango uno *. Sin entrar en demasiados detalles, el "rango" se relaciona con la cantidad de veces que tiene que ir a la izquierda de un -> constructor para encontrar un forall .

Int -> Bool -- rank 0? forall a. (a -> a) -- rank 1 (forall a. a -> a) -> (forall a. a -> a) -- rank 2

En particular, esto restringe un poco el polimorfismo. No podemos escribir algo así con los tipos de rango uno:

foo :: (forall a. a -> a) -> (String, Bool) -- a rank-2 type foo polymorphicId = (polymorphicId "hey", polymorphicId True)

La siguiente restricción más crítica es que las variables de tipo solo pueden reemplazarse por tipos monomórficos. (Esto incluye otras variables de tipo, como a , pero no tipos polimórficos como para todos forall a. a ) Esto garantiza en parte que la sustitución de tipo conserva el rango uno.

Resulta que si haces estas dos restricciones, entonces no solo se puede decidir por inferencia de tipo, sino que también obtienes tipos mínimos .

Si pasamos de Haskell a GHC, podemos hablar no solo de lo que se puede escribir, sino del aspecto del algoritmo de inferencia. En particular, en GHC, hay extensiones que relajan las dos restricciones anteriores; ¿Cómo hace la inferencia GHC en ese contexto? Bueno, la respuesta es que simplemente ni siquiera lo intenta. Si desea escribir términos utilizando esas características, debe agregar las anotaciones de escritura de las que hablamos en el primer párrafo: debe anotar explícitamente dónde se introducen y eliminan todos los elementos. Entonces, ¿podemos escribir un término que el verificador de tipos de GHC rechace? Sí, es fácil: simplemente use los tipos o impredicatividad de rango dos (o superiores) sin anotar. Por ejemplo, lo siguiente no realiza una comprobación de tipo, aunque tiene una anotación de tipo explícita y se puede escribir con los tipos de rango dos:

{-# LANGUAGE Rank2Types #-} foo :: (String, Bool) foo = (/f -> (f "hey", f True)) id

* En realidad, restringir el rango dos es suficiente para que sea decidible, pero el algoritmo para los tipos de rango uno puede ser más eficiente. Los tres tipos de rango ya le dan al programador la suficiente cuerda para hacer que el problema de inferencia sea indecidible. No estoy seguro de si se conocieron estos hechos en el momento en que el comité decidió restringir a Haskell a los tipos de rango uno.