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.