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

[Conor McBride]

On 21 Jan 2012, at 09:01, Andreas Abel wrote:

> Objection, Sir!
>
> While you have erased the black-height from the Tree data structure  
> now, you need to pass it around in all functions that operate on red  
> black trees.  And in these operations, it not erasable.

That's a fair cop.

> By making Tree an untagged union of red nodes, terminal nodes, and  
> black nodes, you need the black height (and color) to fish the  
> correct union component from the soup.

Correct. I'm doing the old trick of retaining the index at run time,
but deleting everything else that can be deduced from it. So all the
choices in the tree structures that are determined by indices no
longer need storage.

> Thus, I think Jonathan's trick has some right of existence.

I wouldn't disagree.

For my money, there is more value in a universal quantifier with  
(closed)
*erasure* than (open) *irrelevance* (especially if you know how to get
proof irrelevance by other means). If we're going to pick just one of  
the
two, I'd pick erasure. It should be an easy choice: more data in the  
nodes
and an erased index, or a runtime index and more compact data  
depending on
it. Perhaps erasure and irrelevance can both be accommodated, though.

And yes, more clarity is required about open versus closed computation,
and what information is needed where. The truth is that we have (at  
least)
three levels (static, open dynamic, closed dynamic). It would help to  
have
a reusable framework for managing communication between these layers.

Cheers

Conor

>
> Cheers,
> Andreas
>
> On 20.01.12 1:19 PM, Conor McBride wrote:
>>
>> 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/