Я смущен ошибкой, которую я получил в конце сеанса ниже:
$ ghci
GHCi, version 7.10.2: http://www.haskell.org/ghc/ :? for help
Ok, modules loaded: Main.
*Main> :set -XDataKinds
*Main> :t [False, True]
[False, True] :: [Bool]
*Main> :t [False]
[False] :: [Bool]
*Main> :k [False, True]
[False, True] :: [Bool]
*Main> :k [False]
<interactive>:1:2:
Expected kind ‘*’, but ‘False’ has kind ‘Bool’
In a type in a GHCi command: [False]
Почему ошибка?
Будущие эксперименты показывают:
*Main> :k [Int]
[Int] :: *
*Main> :k [Int, Int]
[Int, Int] :: [*]
[Int] может иметь обитаемые значения, поэтому он имеет вид *, но также имеет смысл, что он имеет вид [*].
Немного больше точек данных:
*Main> :k []
[] :: * -> *
*Main> :k [Bool]
[Bool] :: *
Если у вас есть списки уровней уровня только с одним элементом, GHC считает, что это не поднятый список, а обычный конструктор типа списка, примененный к некоторому типу вида *.
Вы должны префикс списка с апострофом, чтобы явно выбрать для снятых списков:
> :k '[False]
'[False] :: [Bool]
Аналогично пустым спискам:
> :k '[]
'[] :: [k]
Как вы заметили:
[Int]может иметь обитаемые значения, поэтому он имеет вид*, но также имеет смысл, что он имеет вид[*]
То, что вы заметили, - это то, что DataKinds имеет неоднозначность в выражениях некоторых типов, если вы просто разрешаете выражения значений для уровня типа. Это очень часто приводит к спискам из-за использования квадратных скобок для списков литералов и типов списков, но это не совсем специфично для списков.
В принципе, текст исходного кода [False] может ссылаться на три разные вещи:
FalseFalseFalseБез DataKinds третьего значения не существует, поэтому компилятор всегда может использовать свои контекстуальные знания о том, произошел ли текст исходного кода [False] в выражении типа или выражении значения. Но оба случая 2 и 3 встречаются в выражениях типа, поэтому это не помогает.
В этом случае мы можем видеть, что [False], поскольку тип "список вещей типа False" не имеет никакого смысла, поскольку конструктор типа [] может применяться только к вещам вида *. Но компилятор должен знать, что вы пытаетесь сказать, прежде чем он может набирать/проверять вещи, чтобы убедиться, что он согласован; мы действительно не хотим, чтобы он пытался несколько возможных интерпретаций, а тип/вид проверял их все, молча принимая, если один из них работает. И в любом случае с небольшим усилием (в соответствии с определением подходящих имен типов и/или использованием PolyKinds для создания конструкторов типов, которые принимают вещи нескольких видов), вы можете придумать ситуацию, когда часть исходного текста имеет все 3 вида значения, изложенного выше, и все 3 могут компилироваться без ошибок.
Итак, чтобы устранить неоднозначность (не нарушая существующий синтаксис, например [Int] для "списка вещей типа Int" ), GHC принимает правило, согласно которому обычные конструкторы без поднятого типа имеют приоритет. Таким образом, [False] на самом деле не означает одноуровневый список уровня; это означает только (бессмысленный) "список типов типа False", что приводит к ошибке вида, которую вы видите.
Но DataKinds также вводит синтаксис для явного запроса другого значения; если вы предшествуете конструктору какого-либо типа с апострофом, тогда GHC знает, что вы ссылаетесь на отмененную версию конструктора значений, а не на любой конструктор с невыдвинутым типом с тем же именем. Например:
Prelude> :k 'False
'False :: Bool
И аналогичным образом, при использовании апострофа в синтаксисе списка литерального списка явно указано, что вы пишете литерал на уровне типа, не записывая тип списка, даже если в списке есть только один элемент. Итак:
Prelude> :k '[False]
'[False] :: [Bool]
Prelude> :k '[Int]
'[Int] :: [*]
Аналогичным образом вы можете использовать его для различения конструктора типа списка вида * -> * и пустого списка типов типов:
Prelude> :k []
[] :: * -> *
Prelude> :k '[]
'[] :: [k]