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

Solution 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.

Solution 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.

Comments

[user782220]

Does this mean that the expression S :: Nat -> Nat is overloaded in that it can refer to S as a data constructor taking an argument of type Nat or S as a type constructor taking an argument of kind Nat? Should your example of data Vec :: Nat -> * be instead data Vec a :: Nat -> * to reflect that Vec takes a type argument?

[Daniel Gratzer]

@user782220 1. Yes 2. No, I deliberately made Vec monomorphic, you could if you wanted to

[user782220]

What do you mean by Vec monomorphic? How does it make sense to speak of data Vec :: Nat -> * without any reference to the argument?

[Daniel Gratzer]

@user782220 Vec only works over Ints. Read the constructors.. It's exactly the same as [Int] + lengths in the types

[user782220]

Not understanding why it makes sense to omit the a I would be equally confused if for example I saw data Maybe = Nothing | Just a instead of data Maybe a = Nothing | Just a.

[Daniel Gratzer]

@user782220 What I have is more like data MaybeInt = Nothing | Just Int. I could have but in the extra type parameter but it makes exactly 0 difference to the subject at hand: Kinds.

[user782220]

But isn't it the case that with data MaybeInt = Nothing | Just Int there is only one type Int. Since there are multiple types of kind Nat wouldn't it make more sense to speak of data Maybe a = Nothing | Just a with some syntax to express the constraint that a should be a type coming from kind Nat. In such a case I still don't see how data Maybe = Nothing | Just a would make sense.

[Daniel Gratzer]

let us continue this discussion in chat

[Jules]

I think the easiest thing to overlook in all of this is that without DataKinds, S and Z are not types, but just type constructors producing the type Nat. With DataKinds, they're types, whose kind is Nat. The fact that they weren't types before means that previously they couldn't be referred to in type signatures, which is what this is all about.

[jpaugh]

@jozefg FWIW, I found your chat comments quite helpful. Thanks for taking the time!

[unhammer]

@Jules, that comment should be an Answer! Typically when I've seen use of -XDataKinds, it's because something requires the constructor in a function signature (or conversely, when you want to know how to put a constructor in a function signature, -XDataKinds is the answer)

[dmvianna]

untyped functional programming at the type level is a great observation.

[stevemao]

"S and Z are not types, but just type constructors producing the type Nat" should be data constructor producing data of type Nat

[Kirill Taran]

@Jules, it is clear that with DataKinds S and Z become types as well. But what are the values of these types?

[Wong Jia Hau]

This is exactly what Simon Peyton Jones says in one of his lecture. See youtu.be/brE_dyedGm0?list=TLPQMTMwNTIwMjGbmPzQCvHwyQ&t=3092