DataKinds Are Not What You Think
DataKinds language extension doesn’t work the way you think it does… probably. Of course I can’t possibly know what mental model you have for
DataKinds. Perhaps you are one of the few who understand its true nature. But I’ve seen experts – yes, type-level Haskell wizards – fall into the trap that I’m about to expose.
How DataKinds are commonly explained
To set the stage, let’s take a look at how
DataKinds are commonly explained.
Matt Parsons in his article “Basic Type Level Programming in Haskell” (2017) writes:
data Nat = Zero | Succ Nat
In plain Haskell, this definition introduces a new type
Natwith two value constructors,
Succ(which takes a value of type
Nat). With the
DataKindsextension, this also defines some extra new tidbits. We get a new kind
Nat, which exists in a separate namespace. And we get two new types: a type constant
'Zero, which has the kind
Nat, and a type constructor
'Succ, which accepts a type of kind
Sandy Maguire in his book “Thinking with Types” (2018) writes:
data Bool = False | True
data Booldefinition above introduces the following things into scope (as usual):
- A type constructor
Boolof kind Type
- A data constructor
- A data constructor
-XDataKindsis enabled, our definition of
Boolalso introduces the following into scope:
- A new kind: Bool
- A promoted data constructor
'Trueof kind Bool
- A promoted data constructor
'Falseof kind Bool
Rebecca Skinner in her article “An Introduction to Type Level Programming” (2021) writes:
data ExampleColor = Red | Green | Blue
Here we’re creating a sum type with constructors
Blue, but thanks to
DataKindswe’re also creating a new Kind with types
The common theme in those explanations is that kinds are created from types, as if there was some duplication happening behind the scenes:
What’s wrong with this explanation?
Prior to GHC 8.0 (2016), this model used to work just fine because types and kinds were indeed entirely separate. But with the introduction of the type-in-type axiom, this picture became outdated and misleading. Here are a few lines of code that do not quite fit within this framework:
type family Sing :: k -> Type class FromSing k where fromSing :: Sing (a :: k) -> k
At first glance, this does not even seem related to the picture above. And yet it reveals a fatal flaw in it. In the type signature for
k a type or a kind?
fromSing :: Sing (a :: k) -> k -- ↑ ↑ -- kind type
Well, the first occurrence is a kind, and the second occurrence is a type! How can one variable be a type and a kind simultaneously? This paradox is resolved by the following mental shift: there are no kinds. You heard that right.
- Pre-8.0: terms have types, types have kinds.
- Post-8.0: terms have types, types have types.
We used to have terms, types, and kinds. Now we’re down to terms and types. Occasionally, however, the old terminology is still convenient. Saying “type of a type” every time is a bit awkward, so we may say “kind” instead. The important thing to keep in mind is that a kind isn’t a thing in itself; a type can be used as a kind.
So in the example above,
k is a type variable. It’s used as a kind in
Sing (a :: k), so we might also call it a kind variable. However, this is a statement about how it’s used, not about what it is.
This suggests the following modification to our understanding of
Compared to the previous model, we now have the type level and the term level, whereas kinds don’t get their own level and are merged into types. This is definitely an improvement, but it’s still incorrect in a subtle way. Since this interpretation of
DataKinds is based on duplication, we end up with two separate
Bools. But are they really distinct?
Building upon our definitions of
FromSing, here are some instances for them:
data SBool (a :: Bool) where STrue :: SBool True SFalse :: SBool False type instance Sing @Bool = SBool instance FromSing Bool where fromSing :: Sing (a :: Bool) -> Bool fromSing STrue = True fromSing SFalse = False
Haskell is no stranger to puns. I could declare
data Proxy a = Proxy and have two proxies in scope: one is a data constructor and the other is a type constructor. So it wouldn’t be unreasonable to assume that the same thing is happening with
Bool: perhaps one is a type and the other one is a kind, yet they are internally distinct. Let me mark type and kind occurrences with different numbers:
data SBool (a :: Bool1) where STrue :: SBool True SFalse :: SBool False type instance Sing @Bool1 = SBool instance FromSing Bool2 where fromSing :: Sing (a :: Bool1) -> Bool2 fromSing STrue = True fromSing SFalse = False
The hypothesis we need to test now is whether GHC thinks that
Bool2 are actually distinct entities. The answer shall reveal itself if we compare the type signature of
fromSing in the class declaration and in the instance:
fromSing :: Sing (a :: k) -> k fromSing :: Sing (a :: Bool1) -> Bool2
We seem to instantiate
Bool1 in one position and to
Bool2 in another. So if we had
Bool the type and
Bool the kind, we would expect a type error of the following form:
• Couldn't match type 'Bool' with kind 'Bool'
… because GHC couldn’t decide what
k stands for. And yet the code above compiles just fine, which leads us to the only possible conclusion: there’s just one
One might wonder: are
False actually duplicated if
Bool isn’t? As long as terms and types are separated, we can’t really tell. A term-level variable can’t occur in a type-level context or vice versa, so we can’t ask the compiler if the term-level
True and the type-level
True are equal. There is currently no way to test this hypothesis. One could indeed argue that promoted data constructors are a mirror image of their term-level counterparts.
Dependent types, however, lead us to a more elegant model:
For now this simplification is out of reach, but, personally, I find it to be a very attractive direction.
DataKinds extension does not create new kinds. Instead, it allows existing types to be used as kinds. This objection isn’t based on vague philosophical grounds but has practical implications, as illustrated by a fairly basic use of singleton types that we covered.