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
Well let's start with the basics
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
.
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 DataKind
s makes the kind system extensible.
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.