有没有理由我们不能使用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

Answer 1

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

是.这正是*意味着什么:它是那种(提升/盒装,我从来不确定那部分)Haskell类型.事实上,尽管它们共享type语法,但其他所有类型都不是真正的类型.而不是*类型的元类型级别类型,而所有其他类型都是元类型级别类型,用于非类型但类型构造函数或完全不同的东西.

(同样,还有一些关于未装箱类型的东西;那些肯定是类型,但我认为这对data构造函数来说是不可能的.)

通常我不会在一个帖子中经常输入"类型"这个词. (3认同)
盒装,未装箱的类型具有类型`#`,这就是为什么你不能在多态函数中使用它们,种类不匹配.还有`？`这是各种类型的顶部和`??`,它是`*`和`#`的润滑. (2认同)

Answer 2

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

它们必须是类型*(或#)的最重要原因是GHC使用的相分离:DataKinds在编译期间被擦除.我们可以通过定义单例GADT数据类型来间接表示它们的运行时:

{-# LANGUAGE DataKinds #-}

data Nat = Z | S Nat

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

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