¿Hay algún tipo de firma que Haskell no pueda verificar?

Question

This paper establece que la inferencia de tipo (llamada "capacidad de tipado" en el documento) en el Sistema F es indecidible. Lo que nunca he escuchado mencionar en otra parte es el segundo resultado del artículo, a saber, que "verificación de tipo" en F también es indecidible. Aquí la pregunta de "comprobación de tipos" significa: dado un término t, tipo T y entorno de escritura A, ¿es derivable la sentencia A ⊢ t : T? Que esta pregunta es indecidible (y que es equivalente a la cuestión de la capacidad de tipado) me sorprende, porque 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, sí), el resultado sobre la comprobación de tipos parece sugerir que hay un término Haskell t y escriba T de tal manera que el compilador no se puede decidir si t :: T es válido. Si ese es el caso, tengo curiosidad por saber qué tipo de términos y ese tipo de términos son ... si no es el caso, ¿qué es lo que estoy malinterpretando?

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

Answer 1

Aquí se muestra un ejemplo de una implementación de nivel de tipo de cálculo de esquí en Scala: http://michid.wordpress.com/2010/01/29/scala-type-level-encoding-of-the-ski-calculus/

El último ejemplo muestra una iteración ilimitada. Si haces lo mismo en Haskell (y estoy bastante seguro de que puedes), tienes un ejemplo para una "expresión no tipificable".

Answer 2

La comprobación del tipo se puede hacer decidible enriqueciendo la sintaxis de forma apropiada. Por ejemplo, en el documento, tenemos lambdas escrito como \x -> e; para marcar-verificar esto, debe suponer el tipo de x. Sin embargo, con una sintaxis enriquecida adecuadamente, esto se puede escribir como \x :: t -> e, lo que elimina las conjeturas del proceso. De manera similar, en el documento, permiten que las lambdas de nivel de tipo sean implícitas; es decir, si e :: t, entonces también e :: forall a. t. Para hacer la verificación de tipo, debe adivinar cuándo y cuántos forall agregar y cuándo eliminarlos. Al igual que antes, se puede hacer esto más determinista mediante la adición de sintaxis: añadimos dos nuevos expresión forma /\a. e y e [t] y dos nueva regla de escritura que dice que si e :: t, entonces /\a. e :: forall a. t, y si e :: forall a. t, entonces e [t'] :: t [t'/a] (donde los corchetes en t [t'/a] son soportes 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 los términos del Sistema F suficientemente anotados? Y la respuesta es sí, gracias a algunas restricciones críticas impuestas por el sistema de tipo Haskell. El más crítico es que todos los tipos son de rango uno *. Sin entrar en demasiados detalles, el "rango" está relacionado 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 como esto con la fila uno tipos:

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

El siguiente restricción más importante es que las variables de tipo sólo pueden ser reemplazados por tipos monomorfas. (Esto incluye otras variables de tipo, como a, pero no tipos polimórficos como forall a. a). Esto asegura, en parte, que la sustitución de tipo preserva la jerarquía.

Resulta que si haces estas dos restricciones, entonces no sólo es de tipo inferencia decidible, pero también llegar mínimos tipos.

Si pasamos de Haskell a GHC, entonces podemos hablar no solo de lo que es tipable, sino de cómo se ve el algoritmo de inferencia. En particular, en GHC, hay extensiones que relajan las dos restricciones anteriores; ¿cómo hace GHC inferencia en ese entorno? Bueno, la respuesta es que simplemente ni siquiera lo intenta. Si desea escribir términos usando esas características, debe agregar las anotaciones de tipeo de las que hablamos desde el primer párrafo: debe anotar explícitamente dónde se introducen y eliminan forall s. Entonces, ¿podemos escribir un término que rechaza el verificador de tipos de GHC? Sí, es fácil: simplemente use los tipos o impredicatividad de rango dos sin anotar. Por ejemplo, el siguiente no se escriba-cheque, aunque tiene un tipo de anotación explícita y es tipificable con rango de dos tipos:-

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

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