haskelltypestype-kinds

Haskell's DataKinds and relation of values, types and kinds


Say I have this:

data Animal = Dog | Cat
:t Dog
Dog :: Animal

Fair enough.

:k Dog

<interactive>:1:1:
    Not in scope: type constructor or class ‘Dog’
    A data constructor of that name is in scope; did you mean DataKinds?

Wasn't expecting that to work since Dog is a value, not a type. You cannot get a kind of a value, only a kind of a type, right?

But, if I do this:

:set -XDataKinds
data Animal = Dog | Cat
:k Dog
Dog :: Animal

What does this mean that you can get a kind of a value?


Solution

  • Nope. You can only get the kinds of types. What -XDataKinds does is take data declarations and give them two meanings: first, it declares a new type and some corresponding value constructors; and second, it declares a new kind and some corresponding type constructors. So with DataKinds on, the following declaration:

    data Animal = Dog | Cat
    

    creates all of the following:

    The three namespaces -- term-level, type-level, and kind-level -- are completely disjoint. In case DataKinds would define a new type in two different ways, you can use a prefix ' to indicate that you want the lifted version. Thus:

    > :set -XDataKinds
    > data Animal = Animal
    > :k Animal
    Animal :: *
    > :k 'Animal
    'Animal :: Animal