Haskell 的 DataKinds 以及值、类型和种类的关系

Question

假设我有这个:

data Animal = Dog | Cat
:t Dog
Dog :: Animal

很公平。

:k Dog

<interactive>:1:1:
    Not in scope: type constructor or class ‘Dog’
    A data constructor of that name is in scope; did you mean DataKinds?

没想到它会起作用，因为 Dog 是一个值，而不是类型。你不能得到一种值，只能得到一种类型，对吗？

但是，如果我这样做:

:set -XDataKinds
data Animal = Dog | Cat
:k Dog
Dog :: Animal

这意味着你可以获得某种值？

Answer 1

不。您只能获取 types 的种类。 -XDataKinds 的作用是获取数据声明并赋予它们两个含义:首先，它声明一个新类型和一些相应的值构造函数；其次，它声明了一个新的种类和一些相应的类型构造函数。因此，在启用 DataKinds 的情况下，声明如下:

data Animal = Dog | Cat

创建以下全部:

• 类型动物
• Animal 类型的值 Dog
• Animal 类型的值 Cat
• 种类动物
• 类型狗类型动物
• 类型猫类型动物

这三个命名空间——术语级别、类型级别和种类级别——是完全不相交的。如果 DataKinds 以两种不同的方式定义新类型，您可以使用前缀 ' 来指示您想要提升的版本。因此:

> :set -XDataKinds
> data Animal = Animal
> :k Animal
Animal :: *
> :k 'Animal
'Animal :: Animal