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

Question

使用 DataKinds，定义如下

data KFoo = TFoo

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

data TFoo = CFoo

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

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

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

data 'TFoo = CFoo

我得到错误

错误的类型或类声明头：TFoo

score 9 · Accepted Answer

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

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

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

score 6 · Accepted Answer

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

*它们必须是 type (or )的最重要原因#是 GHC 采用的相分离：DataKinds在编译期间被擦除。通过定义单例 GADT 数据类型，我们只能间接地在运行时表示它们：

{-# LANGUAGE DataKinds #-}

data Nat = Z | S Nat

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

但是DataKind索引本身仍然不存在运行时。各种类型为相分离提供了一个简单的规则，这对于依赖类型来说不会那么简单（尽管它可能会极大地简化类型级编程）。

2 回答 2