tutorialspoint - learn you a haskell pdf

Haskell Weird Kinds: Tipo de(->) es ??->?->*

Question

Cuando estaba experimentando con tipos de Haskell, y tratando de obtener el tipo de -> , y esto apareció:

$ ghci
...
Prelude> :k (->)
(->) :: ?? -> ? -> *
Prelude> 

En lugar de lo esperado * -> * -> * . ¿Cuáles son los ?? y ? ¿cosas? ¿Significan tipos concretos o "variables amables"? ¿O algo mas?

Answer 1

Estas son extensiones específicas de GHC del sistema tipo Haskell. El informe Haskell 98 especifica solo un sistema tipo simple :

... las expresiones de tipo se clasifican en diferentes tipos, que toman una de dos formas posibles:

El símbolo * representa el tipo de todos los constructores de tipo nullary. Si k1 y k2 son tipos, entonces k1-> k2 es el tipo de tipos que toman un tipo de tipo k1 y devuelven un tipo de tipo k2.

GHC amplía este sistema con una forma de subtipado tipo , para permitir tipos no compartidos , y para permitir que el constructor de funciones sea polimórfico sobre clases. El tipo de celosía que GHC admite es:

             ?
             //
            /  /
          ??   (#)
          / /     
         *   #     

Where:       *   [LiftedTypeKind]   means boxed type
             #   [UnliftedTypeKind] means unboxed type
            (#)  [UbxTupleKind]     means unboxed tuple
            ??   [ArgTypeKind]      is the lub of {*, #}
            ?    [OpenTypeKind]     means any type at all

Definido en ghc/compiler/types/Type.lhs

En particular:

> error :: forall a:?. String -> a
> (->)  :: ?? -> ? -> *
> (//(x::t) -> ...)

¿Dónde en el último ejemplo t :: ?? (es decir, no es una tupla sin caja). Entonces, para citar a GHC, "hay un pequeño subtipo en el nivel amable".

Para las almas interesadas, GHC también admite clases y tipos de coerción ("términos de nivel de tipo que actúan como evidencia de igualdades de tipo", según lo necesite el sistema Fc ) utilizados en GADT, newtypes y familias de tipos.