Запутался в расширении DataKinds

В нерасширенном Haskell объявление

data A = B

определяет два новых объекта, по одному на уровне вычислений и на уровне типа:

1. На уровне типа новый базовый тип с именем A (типа *) и
2. На уровне вычислений появилось новое базовое вычисление с именем B (типа A).

При включении DataKinds объявление

data A = B

теперь определяет четыре новых объекта: один на уровне вычислений, два на уровне типа и один на уровне вида:

1. На уровне вида появился новый базовый вид A,
2. На уровне типа новый базовый тип 'B (типа A),
3. На уровне типа новый базовый тип A (типа *) и
4. На уровне вычислений новое базовое вычисление B (типа A).

Это строгое надмножество того, что у нас было раньше: старое (1) теперь (3), а старое (2) теперь (4).

Эти новые объекты объясняют следующие описанные вами взаимодействия:

:type Zero
Zero :: Nat
:kind 'Zero
'Zero :: Nat
:type 'Zero
Syntax error on 'Zero

Я думаю, понятно, как это объясняет первые два. Последнее объясняется тем, что 'Zero относится к типу - вы не можете запрашивать тип типа, только тип вычисления!

Теперь в Haskell в каждом месте, где встречается имя, из окружающего синтаксиса ясно, предназначено ли это имя для имени уровня вычислений, имени уровня типа или имени уровня типа. По этой причине несколько раздражает необходимость включать галочку в 'B на уровне типа — в конце концов, компилятор знает, что мы находимся на уровне типа, и поэтому не может ссылаться на неподнятый уровень вычислений B. Так что для удобства вам разрешается не ставить галочку, когда это однозначно.

С этого момента я буду различать «внутреннюю часть» — где есть только четыре сущности, описанные выше и которые всегда недвусмысленны, — и «поверхностный синтаксис», который представляет собой материал, который вы вводите в файл и передаете. к GHC, который включает двусмысленность, но более удобен. Используя эту терминологию, в поверхностном синтаксисе можно написать следующие вещи со следующими значениями:

Surface syntax    Level           Back end
Name              computation     Name
Name              type            Name if that exists; 'Name otherwise
'Name             type            'Name
Name              kind            Name
---- all other combinations ----  error

Это объясняет первое взаимодействие, которое у вас было (и единственное, что осталось необъяснимым выше):

:kind Zero
Zero :: Nat

Поскольку :kind должно применяться к объекту уровня типа, компилятор знает, что поверхностное синтаксическое имя Zero должно относиться к объекту уровня типа. Поскольку нет внутреннего имени Zero на уровне типа, вместо этого он пытается использовать 'Zero и получает попадание.

Как это может быть двусмысленно? Обратите внимание, что мы определили две новые сущности на уровне типа с помощью одного объявления. Для простоты введения я назвал новые объекты в левой и правой частях уравнения разными именами. Но давайте посмотрим, что произойдет, если мы просто немного подправим объявление:

data A = A

Мы по-прежнему вводим четыре новых внутренних объекта:

1. Добрый A,
2. Тип 'A (типа A),
3. Введите A (типа *) и
4. Вычисление A (типа A).

Упс! Теперь на уровне типа есть как 'A, так и A. Если вы опустите галочку в поверхностном синтаксисе, будет использоваться (3), а не (2) — и вы можете явно выбрать (2) с поверхностным синтаксисом 'A.

Более того, это не обязательно должно происходить из одного объявления. Одно объявление может создать версию с галочкой, а другую — версию без галочки; Например

data A = B
data C = A

введет внутреннее имя уровня типа A из первого объявления и внутреннее имя уровня типа 'A из второго объявления.

{-# LANGUAGE DataKinds #-} не меняет того, что обычно делает ключевое слово data: оно по-прежнему создает тип Nat и два конструктора значений Zero и Succ. Что делает это расширение, так это то, что оно позволяет вам использовать такие типы, как если бы они были видами, и значения, как если бы они были типами.

Таким образом, если вы используете Nat в выражениях уровня типа, он просто будет использовать его как скучный тип Haskell98. Только если вы используете его в однозначном выражении уровня kind, вы получаете версию вида.

Этот автоматический подъем может иногда вызывать конфликты имен, что, я думаю, является причиной синтаксиса ':

{-# LANGUAGE DataKinds #-}
data Nat = Zero | Succ Nat
data Zero

Теперь Zero сам по себе является простым (пустым) типом данных Zero :: *, поэтому

*Main> :k Zero
Zero :: *

В принципе, благодаря DataKinds, Zero теперь также является типом, унаследованным от конструктора значений Zero :: Nat, но он затмевается data Zero. Таким образом, синтаксис цитирования, который всегда относится к поднятым типам, а не к прямо определенным:

*Main> :k 'Zero
'Zero :: Nat