What is the DataKinds extension of Haskell?

Question

I am trying to find an explanation of the DataKinds extension that will make sense to me having come from only having read Learn You a Haskell. Is there a standard source that will make sense to me with what little I've learned?

Edit: For example the documentation says

With -XDataKinds, GHC automatically promotes every suitable datatype to be a kind, and its (value) constructors to be type constructors. The following types

and gives the example

data Nat = Ze | Su Nat

give rise to the following kinds and type constructors:

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

I am not getting the point. Although I don't understand what BOX means, the statements Ze :: Nat and Su :: Nat -> Nat seem to state what is already normally the case that Ze and Su are normal data constructors exactly as you would expect to see with ghci

Prelude> :t Su
Su :: Nat -> Nat

Answer 1

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.

Answer 2

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.