haskell - 我们不能用 DataKinds 填充类型有什么原因吗？

Question

使用 DataKinds，定义如下

data KFoo = TFoo

介绍种类 KFoo :: BOX和类型 TFoo :: KFoo .为什么我不能继续定义

data TFoo = CFoo

这样 CFoo :: TFoo , TFoo :: KFoo , KFoo :: BOX ?

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

编辑 :当我这样做时，我没有收到错误，因为构造函数和类型共享一个命名空间，但 GHC 允许冲突，因为它将名称消除歧义作为常规类型，而不是提升的构造函数。文档说要以 ' 为前缀引用提升的构造函数。当我将第二行更改为

data 'TFoo = CFoo

我得到错误

Malformed head of type or class declaration: TFoo

Answer 1

Do all constructors need to belong to a type that belongs to the kind *?

是的。这正是 *意思是:这是一种(提升/盒装，我不确定那部分)Haskell类型。事实上，所有其他类型都不是真正的类型，尽管它们共享 type句法。而是 *是类型的元类型级别类型，所有其他类型都是元类型级别的类型，用于不是类型而是类型构造函数或完全不同的东西。

(同样，还有一些关于未装箱类型的东西；这些肯定是类型，但我认为这对于 data 构造函数是不可能的。)