Haskell Weird Kinds: Вид (->) есть? ->? -> *

Question

Когда я экспериментировал с Haskell видов, и пытается получить вид ->, и это обнаружился:

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

Вместо ожидаемого * -> * -> *. Что такое ?? и ?? Имеют ли они в виду конкретные типы или «переменные вида»? Или что-то другое?

Answer 1

Это GHC-специфические расширения системы типа Haskell. Haskell 98 Отчет specifies only a simple kind system:

... Выражения типа классифицируются в различные виды, которые принимают один из двух возможных форм:

Символ * представляет собой вид все нульарные конструкторы типа. Если k1 и k2 являются видами, то k1-> k2 - типы типов , которые относятся к типу вида k1 и возвращают тип вида k2.

GHC extends this system с формой любезных подтипов, чтобы unboxed types и разрешить функцию construtor полиморфной над видами. Вид решетки GHC поддерживает это:

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

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

Определено в ghc/compiler/types/Type.lhs

В частности:

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

Где в последнем примере t :: ?? (т.е. не является распакованный кортеж). Итак, чтобы процитировать GHC, «есть небольшой подтипирование на уровне уровня».

Для заинтересованных душ GHC также поддерживает типы и виды принуждения («термины на уровне типа, которые действуют как доказательство эквивалентности типов», по мере необходимости System Fc), используемые в GADT, типах новых типов и типах.