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

Question

Я изучаю программирование типов в Haskell из Базовое программирование на уровне типов в Haskell , но когда оно вводит расширение DataKinds, в этом примере есть что-то странное:

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

Сейчас, Nat повышен до Kind, это нормально.Но как насчет Zero и Succ?

Я пытаюсь получить некоторую информацию от GHCi, поэтому я набираю:

:kind Zero

это дает

Zero :: Nat

это нормально, Zero это тип имеет вид Nat, верно?и я пытаюсь:

:type Zero

он по-прежнему дает:

Zero :: Nat

, что означает, что Zero имеет тип Nat, что невозможно, так как Nat является видом, а не типом, право?Является ли Nat одновременно типом и типом?

И еще одна запутанная вещь: выше в блоге также упоминалось, что при создании Nat вида появляются два новых типа: 'Zero и 'Succ создаются автоматически.Когда я попробую это снова из GHCi:

:kind 'Zero

дает

'Zero :: Nat

и

:type 'Zero

дает

 Syntax error on 'Zero

Хорошо, этодоказывает, что 'Zero является типом.но какова цель создания 'Zero и 'Succ' ??

Answer 1

В нерасширенном 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. Kind A,
2. Тип 'A (типа A),
3. Тип A (типа *) и
4. Вычисление A (типа A).

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

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

data A = B
data C = A

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

Answer 2

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

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

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

{-# 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