Когда я экспериментировал с типами Haskell и пытался получить вид ->, и это показало:
$ ghci
...
Prelude> :k (->)
(->) :: ?? -> ? -> *
Prelude>
Вместо ожидаемого * -> * -> *.
Что такое ?? и ?? Имеют ли они в виду конкретные типы или "переменные вида"? Или что-то еще?
Это GHC-специфические расширения системы типа Haskell. Отчет Haskell 98 указывает только простую систему типов:
выражения типа... классифицируются в разные виды, которые принимают один двух возможных форм:
Символ * представляет собой вид все конструкторы нулевого типа. Если k1 и k2 - виды, то k1- > k2 - это типы типов, которые относятся к типу k1 и вернуть тип вида k2.
GHC расширяет эту систему с помощью формы подтипирования вида, чтобы 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, типах новых типов и типах.