Bug in Data.Map

[Jim Apple]

Even the original paper (1973) describing trees of bounded balance had
a bug! I think it is fair to describe maintaining balance in BBSTs as
"subtle".

Some ideas that might help:

1. http://www.brics.dk/BRICS/ALCOM-FT/TR/ALCOMFT-TR-01-167.html

2. This seems like a place where calling in a theorem prover might be
appropriate:

(a) The operations are tricky
(b) The data structure is very important
(c) Coq has done similar work before:
http://www.lri.fr/~filliatr/fsets/ (The performance suffered, but I
think all of that can be alleviated with Coq's updated extraction
mechanism. Pragmas necessary for performance would still need to be
inserted after extraction.)

On Tue, Aug 3, 2010 at 4:59 PM, Daniel Peebles <pumpkingod at gmail.com> wrote:
> Deletion in Data.Map does not always preserve the balance of a tree.