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

[Andreas Abel]

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.

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.

To get tagged red-black trees as in Haskell, we can fall back to the 
good old encoding of inductive families by inductive types:

data RBTree (c : Color)(n : ℕ) : Set where

   leaf      : c ≡ black → n ≡ zero → RBTree c n

   redNode   : c ≡ red →
                 RBTree black n → Key → RBTree black n → RBTree c n

   blackNode : c ≡ black → (m : ℕ) → n ≡ suc m → (c' : Color) →
                 RBTree c' m → Key → RBTree c' m → RBTree c n

However, currently there is no means to declare m as erasable, and the 
theory to make it irrelevant is not there yet (and I do not know whether 
it can be sound).

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

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/