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...