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

沒有。你只能得到各種類型。 -XDataKinds做的是取數據聲明並給他們兩個的含義：首先，它聲明一個新類型和一些相應的值構造函數;其次，它聲明一個新的種類和一些相應的類型構造函數。因此，與DataKinds上，以下聲明：

data Animal = Dog | Cat 

創建以下的所有：

• 型Animal
• 值類型的類型DogAnimal
• 價值CatAnimal
• 種Animal
• 的那種Animal

樣Animal

型Cat的Dog型三種命名空間 - 長期層次，類型，層次和類型的級別 - 是完全脫離。在DataKinds將以兩種不同方式定義新類型的情況下，可以使用前綴'來指示您想要提升版本。因此：

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