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

[Alan Jeffrey]

On 01/19/2012 10:52 PM, jleivent at comcast.net wrote:
> Would the black-level terms have been erasable by the compiler had I used normal naturals?

This depends on the back end, as Agda's IL doesn't handle much in the 
way of optimization.

The JS back end does some very simplistic analysis of "singleton types", 
types with at most one closed inhabitant. These are zero-field records, 
zero-constructor datatypes, datatypes with one zero-argument 
constructor, functions to singleton types, and Set. Many expressions of 
singleton type are erased, and replaced by the singleton.

So in this case, all the uses of naturals in red-black tree types would 
be erased, but rather annoyingly there's no dead-code analysis, so the 
natural expressions would still be there. Moreover, I'd expect that in 
most cases the dead-code analysis would have to be a whole-program 
analysis, so can't be performed by the Agda compiler (it would need to 
be done by the JS JIT compiler).

A.