Quantifiers: Dark Matter

Modern cosmology routinely deals with dark matter, a source of gravity necessary to explain certain things. In the last days I discovered a kind of dark matter in Ωmega too, and here is the related story.

As we know type constructors arise when the data definition is equipped with parameters, like below:

data Tree a = Tip a | Fork (Tree a) (Tree a)

a is a type variable and gets instantiated (to a type) when we want the tree to contain actual information.

Actually I could have written the second recursive occurrence of Tree a in the Fork branch as Tree Char, and the type checker would have accepted it. Why? Because at each instantiation site the type variable a is created fresh, and can be bound to a new expression.

But what is the kind of a? In Haskell it can only be *, which classifies all types, as the other possible kinds (* → *, etc.) do not classify types. But this kinding relation is not spelled out directly, so let's choose a more explicit definition:

data Tree :: * → * where ...

When talking about Tree Integer, then it gets pretty clear that Integer's kind must be * and that the resulting Tree Integer is itself kinded by *.
But there is a fine distinction between explicit and implicit kinding in Ωmega: in the latter case a is kinded by a unification variable instead of by *. The reason is that Ωmega allows us to define custom kinds, which can classify other type-like things. These are usually used for indexing of type constructors.

The unification variables that are present, but hidden from the user only become manifest when we have multiple levels of data definitions, with the higher levels indexing the lower ones and some constructor function tries to bind the unification variable to different kinds. Of course that won't work and all you'll see is a very cryptic error message. The smallest example I have encountered is issue 70, which I will present as an example here.


data Pat :: *3 where
  Q :: Pat ~> Pat

data Pat' :: Pat ~> *2 where
  Q' :: Pat' n ~> Pat' (Q n)

data Pat'' :: Pat' p ~> *1 where
  Q'' :: Pat'' n ~> Pat'' (Q' n)

data Pat''' :: Pat'' p ~> *0 where
  Q :: Pat''' n → Pat''' (Q'' n)

Look at the last line, it induces these two kind equations:

n = Pat'' p1
Q'' n = Pat'' p2

Each equality at some level induces an equality at one level up. But p1 and p2 are kinded by the same unification variable, k. Let's note the two equations with k in the middle:

m = k = Q' m

where m is the kind of n.
You can see now that m is forced to be equal to Q' m, which is clearly incommensurable.
The solution is clearly to spell out kinding quantifiers explicitly with type variables. Since these get instantiated to fresh copies on the fly, the above problem does not occur.

So we arrive at (only showing the last definition for brevity's sake)

data Pat''' :: forall (o::Pat) (p::Pat' o) . Pat'' p ~> *0 where
  Q :: Pat''' n → Pat''' (Q'' n)

Black magic? Only when you let the kinds live in the dark!