Is there a reason we can't populate types with DataKinds?

Question

With DataKinds, a definition like

data KFoo = TFoo

introduces the kind KFoo :: BOX and the type TFoo :: KFoo. Why can't I then go on to define

data TFoo = CFoo

such that CFoo :: TFoo, TFoo :: KFoo, KFoo :: BOX?

Do all constructors need to belong to a type that belongs to the kind *? If so, why?

Edit: I don't get an error when I do this, because constructors and types share a namespace, but GHC permits conflicts because it disambiguates names as regular types, rather than promoted constructors. The docs say to prefix with a ' to refer to the promoted constructor. When I change that second line to

data 'TFoo = CFoo

I get the error

Malformed head of type or class declaration: TFoo

What error do you get when you try to define `data TFoo`? – cdk Jun 26 '14 at 20:42 — cdk, Jun 26 '14 at 20:42

leftaroundabout · Accepted Answer · 2014-06-26T20:52:24.533

9

Do all constructors need to belong to a type that belongs to the kind *?

Yes. That's exactly what * means: it's the kind of (lifted / boxed, I'm never sure about that part) Haskell types. Indeed all other kinds aren't really kinds of types though they share the type syntax. Rather * is the metatype-level type for types, and all other kinds are metatype-level types for things that aren't types but type constructors or something completely different.

(Again, there's also something about unboxed-type kinds; those certainly are types but I think this isn't possible for a data constructor.)

edited Jun 26 '14 at 20:52

answered Jun 26 '14 at 20:46

leftaroundabout

117,950
5
174
319

3

Typically I wouldn't type the word "type" so often in a single post. – leftaroundabout Jun 26 '14 at 20:47
1

`*` is kind of all lifted types and `#` is unlifted. `*` and `#` together encapsulate all types which have values. Boxed just refers to if something is a pointer or not, I believe. – user2407038 Jun 26 '14 at 23:31
2

Boxed, unboxed types have the kind `#` which is why you can't use them in polymorphic functions, kind mismatched. There's also `?` which is the top of all kinds and `??` which is the lub of `*` and `#`. – daniel gratzer Jun 27 '14 at 04:49

score 6 · Answer 2 · answered Jun 26 '14 at 21:20

Do all constructors need to belong to a type that belongs to the kind *? If so, why?

The most important reason why they must be of type * (or #) is the phase separation employed by GHC: DataKinds get erased during compilation. We can represent them runtime only indirectly, by defining singleton GADT datatypes:

{-# LANGUAGE DataKinds #-}

data Nat = Z | S Nat

data SNat n where
   SZ :: SNat Z
   SS :: SNat n -> SNat (S n)

But the DataKind indices themselves still don't exist runtime. The various kinds offer a simple rule for phase separation, which wouldn't be as straightforward with dependent types (even though it would potentially simplify type level programming greatly).

Is there a reason we can't populate types with DataKinds?

2 Answers2