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!

Hats off

The types subreddit references Chuan-kai Lin's PhD thesis about GADT type inference. I already have read the pointwise paper, but this is of course a revelation. He actually did implement an algorithm that inferred types for 25 (out of 30) little benchmark programs with GADTs. Previous attempts accomplished at most one!

But the thing that impressed me the most wasn't the technical side of his story but the beautifully crafted slides of his PhD defense talk. I am baffled...

Congratulations Chuan-kai!

Sized types

I have always liked the idea of assigning some notion of size to (tree-like) values, and track its changes along pattern matching and construction to be able to reason about termination-unaffecting recursive calls.

Many years ago, when reading the Hughes-Pareto-Sabry paper I did not see the point yet why termination is fundamental in various aspects.

Only when sitting on the park bench on the isle of Margitsziget (Budapest) and discussing with Tim about sound logic in Ωmega, it dawned to me how termination checking with sized types can be exploited.

I developed the intuition of the tree-like data floating heads down in the water and we are reasoning about criteria that it can still float without touching the ground at depth n. Still, this metaphor was rather hazy.

In the meantime I have tried to digest the relevant papers from Barthe and Abel, brainstormed somewhat here and let my brain background.

Yesterday, I found (on reddit) a link to Abel's new MiniAgda implementation and its description. It made clear to me that my early intuition was not bad at all, the water depth is the upper limit of the size, and recursion is to reduce this to obtain a well-founded induction.

Now it is time to rethink my ideas about infinite function types and how they can be reconciled with sized types.

But it looks like Abel has done the hard work and his Haskell implementation of MiniAgda could be married with Ωmega in the following way: Derive a sized variant of every (suitable) Ωmega datatype and try to check which functions on them terminate. These can be used as theorems in Ωmega.

Hopefully Tim is paying attention to this when implementing Trellys...

Comonads

Slowly recovering from vacation-induced ignorance, today I printed out some interesting papers about type-preserving compilation, plans for type-level functions in GHC and dataflow implementations using comonads. Another one about Hoare Type Systems remained on my screen, too heavy for me, a.t.m.
So I am wrapping my head around category theory again. Somehow all these topics seems to interact, and I continuously am trying to fit them into my Thrist framework. Today I tried to implement a Comonad to Thrist adapter (in my mind at least, no code written yet).

Tail Merging in Ωmega

Today finally I got around improving my Cat-like language optimizer with a new twist:
I can finally factor out common instructions from the end of the two If legs and prepend them to the If's continuation. This wouldn't be an interesting achievement if it wouldn't be written in Ωmega's type-pedantic fragment. To wit:

• tailMerge False [If [Dup]l [Dup]l, Print]l (revThrist' [Dup]l) (revThrist' [Dup]l) [Print]l
• becomes: [(PopN 1v),Dup,Print]l : forall a (b:Prod *0).Thrist Cat [Bool,a; b]sh [a; b]sh

If you think the above lines are in Chinese, you can stop now. If you discover that the If has completely been eliminated and replaced by popping a boolean and duplicating the TOS, then you are pretty good in reading obscure code.
The funny thing is that all the types of values that are on the stack are painstakingly tracked, and the transformation is automatically type correct in Cat because it is type checked in the metalanguage.

I am sure that similar transformations have been proven type correct (and thus pretty correct) before, however I would like to know whether this particular optimization has been already formalized using expressive types.

The big surprise for me was the fact that writing down the transformation only needed a dozen lines of code, support functions included. Of course, my proof of concept only matches on Dup instructions, but the rest is basically boilerplate.

The second surprise is, that so far I did not need a single theorem declaration, an indication that either I am still in very shallow waters regarding the power of Ωmega's typechecker, or my Thrist construction is so clever that it provides enough type hints to the narrowing engine to deduce all types.

I am in the process of writing a paper on all this, and - as always - need some encouragement. Tail merging will definitely belong to the beef part of it.