我们为什么不能使用DataKinds来填充类型？

Question

使用 DataKinds，可以如下定义:

data KFoo = TFoo

介绍了类型 TFoo :: KFoo 和类别 KFoo :: BOX。那么我为什么不能接着定义

data TFoo = CFoo

如何满足CFoo :: TFoo，TFoo :: KFoo，KFoo :: BOX？

所有构造函数是否需要属于属于类型*的种类？如果是这样的话，为什么？

编辑：我这样做时不会出现错误，因为构造函数和类型共享命名空间，但GHC允许冲突，因为它将名称作为常规类型进行消歧义，而不是晋升的构造函数。文档建议使用'前缀来引用晋升的构造函数。当我将第二行更改为

data 'TFoo = CFoo

我遇到了以下错误：

类型或类声明的头部格式不正确：TFoo

- Dan

---

当您尝试定义 data TFoo 时，会出现什么错误？ - cdk

Answer 1

所有构造函数都需要属于属于类型*的种类吗？

是的。这正是*的含义：它是Haskell类型的（提升/装箱，我对这一部分从来不确定）种类。实际上，所有其他种类并不真正是类型的种类，尽管它们共享type语法。相反，*是类型的元类型级别，而所有其他种类都是元类型级别的类型，用于表示不是类型但是类型构造函数或完全不同的东西。

（再次提醒，还有关于未装箱类型种类的一些内容；这些肯定是类型，但我认为这对于data构造函数是不可能的。）

- leftaroundabout

---

通常我不会在一篇帖子中频繁地输入“type”这个词。 - leftaroundabout

* 代表所有提升类型，# 代表非提升类型。* 和 # 共同封装了所有具有值的类型。Boxed 只是指是否为指针，我相信。 - user2407038

Boxed、unboxed类型具有＃种类，因此您无法在泛型函数中使用它们，类型不匹配。还有？，它是所有种类的顶部和？？，它是*和＃的lub。 - daniel gratzer

Answer 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 的索引本身仍然不存在于运行时。各种类型提供了一个简单的阶段分离规则，这在依赖类型下可能不那么直接（即使它有可能极大地简化类型级编程）。

- András Kovács