haskelltypesalgebraic-data-typesdata-kinds

What is the DataKinds extension of Haskell?


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

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