Почему: k [False] приводит к ошибке в GHCI?

Ответ 1

Если у вас есть списки уровней уровня только с одним элементом, GHC считает, что это не поднятый список, а обычный конструктор типа списка, примененный к некоторому типу вида *.

Вы должны префикс списка с апострофом, чтобы явно выбрать для снятых списков:

> :k '[False]
'[False] :: [Bool]

Аналогично пустым спискам:

> :k '[]
'[] :: [k]

Ответ 2

Как вы заметили:

[Int] может иметь обитаемые значения, поэтому он имеет вид *, но также имеет смысл, что он имеет вид [*]

То, что вы заметили, - это то, что DataKinds имеет неоднозначность в выражениях некоторых типов, если вы просто разрешаете выражения значений для уровня типа. Это очень часто приводит к спискам из-за использования квадратных скобок для списков литералов и типов списков, но это не совсем специфично для списков.

В принципе, текст исходного кода [False] может ссылаться на три разные вещи:

• Список литерального синтаксиса для списка значений значений, содержащий один элемент, который является значением False
• Конструктор типа списка применяется к типу False
• Список литерального синтаксиса для списка уровней типов, содержащий один элемент, который является типом False

Без 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]