[Agda] red black trees with delete

Andreas Abel andreas.abel at ifi.lmu.de
Wed Jan 11 15:43:08 CET 2012

Hello Jonathan,

you might be interested to compare your solution to Julien Oster's.



On 1/11/12 2:04 PM, Nils Anders Danielsson wrote:
> On 2012-01-11 03:36, jleivent at comcast.net wrote:
>> Since I'm a novice at dependent-typed programming, I'm not sure if
>> this is a trivial result or not. However, one interesting thing is
>> that I didn't previously know or refer to any existing red black tree
>> implementation of delete - I just allowed the combination of the Agda
>> type checker and the exacting dependent type signatures to do their
>> thing (with some simple reasoning about what the delete function must
>> contain - such as a delete minimum function) - making me feel more
>> like a facilitator than a programmer.
> I had a similar experience when implementing the AVL trees in the
> standard library. I had never implemented tree rotations, but once I had
> the types in place (at that time primarily balancing information) the
> rotations almost wrote themselves.

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

More information about the Agda mailing list