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

[Conor McBride]

On 20 Jan 2012, at 09:51, Andreas Abel wrote:

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

You can eliminate black-height storage entirely without using
irrelevance by using computation. This method works in general
for data indexed over some (possibly large?) I.

First, define the pattern functor of your indexed set

F : (I -> Set) -> (I -> Set)

as a function which computes the choice of constructions
from the index.

e.g. (with I = Col * Nat)

F X (red , n) = X (black , n) * Key * X (black , n)
F X (black , zero) = One
F X (black , suc n) =
   Sig Col \ c -> X (c , n) * Key * Sig Col \ c -> X (c , n)

That's conspicuously strictly positive in X. So you can take
a fixpoint

data Tree (i : I) : Set where
   [_] : F Tree i -> Tree i

As left-of-colon indices (sometimes ignorantly called parameters)
are not stored, you can see that we've eliminated height storage
entirely, and colour storage only in black nodes, where there is
a genuine choice (and the information is needed at run time).

How times change. I used to be the only person who wanted inductive
families with constrained constructors. Now I'm one of the few who
wants to ban them.

Cheers

Conor


>
> 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/
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda