Haskell 的 DataKinds 扩展是什么？

我试图找到一个 DataKinds 扩展的解释，这对我来说是有意义的，因为我只读过 向你学习 Haskell。有没有一个标准的资料来源，可以让我用我所学到的一点点东西来解释这个问题？

编辑: 例如 文件说

通过 -XDataKinds，GHC 自动提升每个合适的数据类型 类型，其(值)构造函数为类型构造函数。 以下类型

并给出了例子

data Nat = Ze | Su Nat

产生下列种类和类型构造函数:

Nat :: BOX
Ze :: Nat
Su :: Nat -> Nat

我不明白。虽然我不明白 BOX的意思，但是语句 Ze :: Nat和 Su :: Nat -> Nat似乎说明了通常情况下 Zeand Su 是正常的数据构造函数，正如您期望在 ghi 中看到的那样

Prelude> :t Su
Su :: Nat -> Nat
23545 次浏览
小开
最佳答案

Well let's start with the basics

Kinds

Kinds are the types of types*, for example

Int :: *
Bool :: *
Maybe :: * -> *

Notice that -> is overloaded to mean "function" at the kind level too. So * is the kind of a normal Haskell type.

We can ask GHCi to print the kind of something with :k.

Data Kinds

Now this is not very useful, since we have no way to make our own kinds! With DataKinds, when we write

 data Nat = S Nat | Z

GHC will promote this to create the corresponding kind Nat and

 Prelude> :k S
S :: Nat -> Nat
Prelude> :k Z
Z :: Nat

So DataKinds makes the kind system extensible.

Uses

Let's do the prototypical kinds example using GADTs

 data Vec :: Nat -> * where
Nil  :: Vec Z
Cons :: Int -> Vec n -> Vec (S n)

Now we see that our Vec type is indexed by length.

That's the basic, 10k foot overview.

* This actually continues, Values : Types : Kinds : Sorts ... Some languages (Coq, Agda ..) support this infinite stack of universes, but Haskell lumps everything into one sort.

小开

Here is my take:

Consider a length indexed Vector of type:

data Vec n a where
Vnil  :: Vec Zero a
Vcons :: a -> Vec n a -> Vec (Succ n) a


data Zero
data Succ a

Here we have a Kind Vec :: * -> * -> *. Since you can represent a zero length Vector of Int by:

Vect Zero Int

You can also declare meaningless types say:

Vect Bool Int

This means we can have untyped functional programming at the type level. Hence we get rid of such ambiguity by introducing data kinds and can have such a kind:

Vec :: Nat -> * -> *

So now our Vec gets a DataKind named Nat which we can declare as:

datakind Nat = Zero | Succ Nat

By introducing a new data kind, no one can declare a meaningless type since Vec now has a more constrained kind signature.


提交答案