Haskell Странные Виды: Отчасти (->)??->?-> *

Question

Haskell Странные Виды: Отчасти (->)??->?-> *

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

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

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

65

haskell types type-systems

задан Dan Burton 3 December 2011 в 21:45

1 ответ

Другие вопросы по тегам:

haskell types type-systems

Похожие вопросы:

score 96 · Accepted Answer

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

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

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

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