[Agda] Erasable vs. irrelevant, and red black trees again

[Adam Gundry]

Hello,

On 20/01/12 04:52, jleivent at comcast.net wrote:
> Would the black-level terms have been erasable by the compiler had I
> used normal naturals?  Would the use of the normal "strong"
> discrimination between zero and suc n for naturals by the type
> checker when eliminating those impossible cases in bal1 and bal2 have
> prevented the erasure?

It is certainly possible to implement red-black trees without access to
the black height at runtime, but it might be difficult to communicate to
the computer that you are doing so. Agda doesn't make it easy to keep
track of what will be erased: while one can sometimes use the
irrelevance machinery, it's not a perfect fit.

You might be interested in Edwin Brady's work on erasure [1], notably
his thesis and the paper "Inductive Families Need Not Store Their
Indices". The Epic backend for Agda implements some of his optimisations.

<self-promotion> On erasure of natural numbers specifically, you could
also look at Inch [2], my typechecker for a dialect of Haskell with
type-level integers. It is a preprocessor that erases the type indices
before compilation, so they are definitely absent at runtime. I've
implemented red-black trees [3] based on the Agda code I posted before.
Of course, Inch only supports a very limited form of dependent types, so
one can't verify as much as your code does. </self-promotion>

All the best,

Adam


[1] http://edwinb.wordpress.com/publications/
[2] https://github.com/adamgundry/inch/
[3] https://github.com/adamgundry/inch/blob/master/examples/RedBlack.hs