Хаскель странные виды: вид (->) это ?? ->? -> * - PullRequest
Новая
       17

Хаскель странные виды: вид (->) это ?? ->? -> *

65 голосов
/ 14 июня 2010

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

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

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

1 Ответ

96 голосов
/ 14 июня 2010

Это специфичные для GHC расширения системы типа Haskell. В отчете Haskell 98 указывается только простая система вида :

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

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

GHC расширяет эту систему в форме подтипов вида, чтобы разрешить распакованные типы и позволить полимеру функции 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, новых типах и семействах типов.

...