valores - tipos de datos en haskell

Por qué la restricción de clase en el sinónimo de tipo necesita RankNTypes

Question

Esto compila bien:

type List a = [a]

Pero cuando introduzco una restricción de clase, el compilador pide que se incluya RankNTypes :

type List2 a = Num a => [a]

Después de incluir esa extensión, compila bien. ¿Por qué se necesita esa extensión para compilar el código?

Edit: ¿Por qué necesito la restricción en primer lugar?

Estaba inspeccionando este tipo de lente ( type RefF ab = Functor f => (b -> fb) -> (a -> fa) ) de esta publicación y descubrí que realmente necesitaba RankNTypes debido a la restricción de Functor .

Answer 1

No es estandar

En el que se responde la pregunta.

La respuesta simple es que Haskell estándar no permite declaraciones de sinónimo de tipo calificado, es decir, un sinónimo de tipo que implica => . Según el informe de 2010 , la sintaxis de una declaración de sinónimo de tipo es:

type simpletype = tipo

donde type , si observa la Sección 4.1.2, no puede contener un contexto.

Por cierto, la presencia de la variable de tipo a en el contexto no importa. Sin extensiones, GHC rechaza.

type IrrelevantConstraint a = Num Int => [a]

o, para el caso,

type QualifiedT = Num Int => String

Además, incluso si se permitiera tal tipo de sinónimo, ningún uso no trivial sería Haskell estándar, como lo demuestra la sustitución manual:

List2 a      === forall a.   Num a => [a]        -- Okay
List2 a -> b === forall a b. (Num a => [a]) -> b -- Not okay
a -> List2 b === forall a b. a -> Num b => [b]   -- Not okay

Y así sucesivamente para Maybe (List2 a) etc. En cada caso, no es que sea un tipo de rango superior en el sentido habitual. He agregado explícitamente para toda notación, que por supuesto tampoco es estándar, para enfatizar ese hecho.

Más bien, el problema es que cada tipo se califica de forma inadecuada porque => aparece dentro del tipo. Nuevamente, si observa las secciones del Informe 2010 sobre firmas y declaraciones de tipo de expresión , verá que => no es estrictamente hablando parte de un tipo , sino más bien una cosa sintácticamente distinta, por ejemplo:

exp → exp :: [ context => ] type

Dado que List2 no es válido Haskell2010, es necesaria alguna extensión de idioma para que funcione. No se documenta específicamente que RankNTypes permita declaraciones de sinónimos de tipo calificados, pero como ha notado, tiene ese efecto. ¿Por qué?

Hay una pista en los documentos de GHC en RankNTypes :

La opción -XRankNTypes también se requiere para cualquier tipo con un forall o contexto a la derecha de una flecha (por ejemplo, f :: Int -> forall a. a->a , o g :: Int -> Ord a => a -> a ). Dichos tipos son técnicamente de rango 1, pero claramente no son Haskell-98, y una bandera adicional no parece ser la molestia.

El ejemplo de g está relacionado con nuestro problema de List2 : no hay nada allí, pero hay un contexto a la derecha de una flecha, que es el tercer ejemplo que mencioné anteriormente. A medida que sucede, RankNTypes habilita el segundo ejemplo también.

Un viaje lateral a través de Template Haskell.

En el que se toma un desvío que se puede omitir, el Sr. Forall se descubre en un lugar inesperado y se ponderan los rangos y contextos.

No sé si la representación de una declaración de Haskell de la Plantilla está necesariamente vinculada a la representación u operación interna del buscador de tipo. Pero encontramos algo un poco inusual: un lugar donde no esperaríamos, y sin variables de tipo:

> import Language.Haskell.TH
> :set -XTemplateHaskell
> runQ [d|type List2 a = Num a => [a]|]
[TySynD List2_2
        [PlainTV a_3]
        (ForallT []
                 [ClassP GHC.Num.Num [VarT a_3]]
                 (AppT ListT (VarT a_3)))]

-- simpler example:
> runQ [d|type T = Num Int => Int|]
[TySynD T_0
        []
        (ForallT []
                 [ClassP GHC.Num.Num [ConT GHC.Types.Int]]
                 (ConT GHC.Types.Int))]

Lo notable aquí es el ForallT aparentemente espurio. En la plantilla Haskell, esto tiene sentido porque ForallT es el único constructor de Type con un campo Cxt , es decir, que puede contener un contexto. Si el buscador de caracteres combina de manera similar todos los contextos y restricciones, tendría sentido que RankNTypes afectara su comportamiento. Pero lo hace?

Como implementado en GHC

En el cual se descubre por qué RankNTypes permite List2

El error preciso que obtenemos es:

Illegal polymorphic or qualified type: Num a => [a]
Perhaps you intended to use RankNTypes or Rank2Types
In the type declaration for `List2''

La búsqueda a través de la fuente GHC revela que este error se genera en TcValidity.hs . El punto de entrada que nos interesa es checkValidType .

Podemos verificar que el compilador realmente ingresa allí compilando con -ddump-tc-trace ; La última salida de depuración antes del mensaje de error es:

Starting validity check [Type constructor `List2'']
checkValidType Num a => [a] :: *

Continuando en checkValidType , vemos que, en ausencia de RankNTypes , el RHS de un sinónimo de tipo debe tener el rango 0 . (Desafortunadamente, la salida de depuración no especifica el valor de ctxt aquí, pero presumiblemente es TySynCtxt ).

La nota que se encuentra justo encima de checkValidType define los rangos en este contexto, por lo tanto:

    basic ::= tyvar | T basic ... basic

    r2  ::= forall tvs. cxt => r2a
    r2a ::= r1 -> r2a | basic
    r1  ::= forall tvs. cxt => r0
    r0  ::= r0 -> r0 | basic

Ese comentario cuadra con el experimento de Template Haskell, es decir, que un tipo de rango 0 no puede incluir => , y cualquier tipo que incluya => debe incluir un forall y, por lo tanto, debe ser de 1 o 2, incluso si no hay variables de tipo en el forall . En la terminología descrita en TcType , los contextos solo aparecen en los tipos sigma.

En otras palabras, tal como se implementó, el typechecker rechaza el RHS de List2 porque interpreta el RHS como rango 1 debido a su calificación de clase.

La rama que conduce a nuestro mensaje de error comienza here . Si entiendo correctamente, theta representa el contexto de restricción. El núcleo de la primera línea del bloque do es para forAllAllowed rank , que hace lo que parece. Recuerde desde arriba que el RHS de un sinónimo de tipo está restringido al rango 0; Ya que un forall no está permitido, obtenemos un error.

Esto explica por qué RankNTypes anula esta limitación. Si rastreamos de dónde proviene el rank del parámetro, a través de rank0 en checkValidType y luego a través de las pocas líneas anteriores, encontramos que el indicador RankNTypes básicamente anula la restricción de rank0 . (Contraste la situación con las declaraciones predeterminadas ). Y como el contexto adicional se trató como un error de clasificación , RankNTypes permite.