Haskell tipos estranhos: Tipo de (->) é ?? -> -> * - haskell, tipos, sistemas de tipos

Quando eu estava experimentando tipos de Haskell e tentando obter o tipo de ->, e isso apareceu:

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

Em vez do esperado * -> * -> *. O que são as ?? e ? coisas? Eles significam tipos concretos ou "variáveis ​​de tipo"? Ou outra coisa?

Respostas:

Estas são extensões específicas do GHC do sistema de tipo Haskell. O relatório Haskell 98 especifica apenas um sistema de tipo simples:

... expressões de tipo são classificadas em diferentes tipos, o que leva um de duas formas possíveis:

O símbolo * representa o tipo de todos os construtores de tipo nulo. Se k1 e k2 são tipos, então k1-> k2 é o tipo de tipo que leva um tipo de tipo k1 e retorna um tipo do tipo k2.

GHC estende este sistema com uma forma de subtipagem, para permitir tipos unboxed, e para permitir que o construtor da função seja polimórfico sobre os tipos. O tipo de rede que o GHC suporta é:

             ?
/
/  
??   (#)
/ 
*   #

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 em ghc / compiler / types / Type.lhs

Em particular:

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

Onde no último exemplo t :: ?? (ou seja, não é uma tupla não encaixotada). Portanto, para citar GHC, "há um pequeno subtipo no nível de tipo".

Para almas interessadas, o GHC também suporta tipos e tipos de coerção ("termos de nível de tipo que atuam como evidência para igualdades de tipo", conforme necessário por Sistema Fc) usado em GADTs, newtypes e famílias de tipo.