Есть ли причина, по которой мы не можем заполнять типы DataKinds?

вводит вид KFoo :: BOX и тип TFoo :: KFoo. Почему я не могу затем определить

Должны ли все конструкторы принадлежать типу, принадлежащему виду *? Если да, то почему?

Изменить. Я не получаю сообщение об ошибке, когда я это делаю, потому что конструкторы и типы совместно используют пространство имен, но GHC разрешает конфликты, поскольку он неоднозначно вызывает имена как обычные типы, а не рекламируемые конструкторы. Документы говорят, чтобы префикс с ' ссылался на продвигаемый конструктор. Когда я меняю эту вторую строку на

Ответы

Ответ 1

Должны ли все конструкторы принадлежать типу, который принадлежит типу *?

Да. То, что означает *: это тип (снятый/в коробке, я никогда не уверен в этой части) типы Haskell. Действительно, все остальные типы не являются действительно типами типов, хотя они разделяют синтаксис type. Скорее * - тип уровня метатипа для типов, а все другие типы - типы уровня метатипа для вещей, которые не являются типами, но конструкторы типов или что-то совершенно другое.

(Опять же, есть что-то типа unboxed-type, это, конечно, типы, но я думаю, что это невозможно для конструктора data.)

Ответ 2

Должны ли все конструкторы принадлежать типу, принадлежащему виду *? Если да, то почему?

Самой важной причиной, по которой они должны быть типа * (или #), является разделение фаз, используемое GHC: DataKinds стирается во время компиляции. Мы можем представлять их время выполнения только косвенно, определяя типы данных Singleton GADT:

{-# LANGUAGE DataKinds #-}

data Nat = Z | S Nat

data SNat n where
   SZ :: SNat Z
   SS :: SNat n -> SNat (S n)

Но сами индексы DataKind все еще не существуют. Различные типы предлагают простое правило для разделения фаз, которое не было бы столь же простым с зависимыми типами (хотя это могло бы значительно упростить программирование уровня).