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

[Andreas Abel]

Hello Jonathan,

thanks for posting the code.  The parametrization is a nice-trick to get 
erasable black-heights.  Ideally, you could do this with irrelevance 
also, but the theory and implementation is not there yet.

Cheers,
Andreas

On 20.01.12 5:52 AM, jleivent at comcast.net wrote:
> Here is the red-black tree code I sent in last week, updated (and
> re-arranged a bit) with this concept of erasable Naturals I've been
> discussing with you, so that each node in the red-black tree isn't
> carrying any extra baggage at runtime - just the necessary red/black
> color flag (and its subtrees, of course).
>
> The bal1 and bal2 functions demonstrate the use of that "weak-disc"
> axiom.  Comments in bal1 explain the usage.  Hopefully this will
> clarify things.
>
> 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?
>
> -- Jonathan Leivent

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/