Bug in the proof of Data.FiniteMap and DData.Map

[Robert Will]

hi,

both of the data structures are based on Adams' balancing algorithm
which contains a bug -- at least in its proof.  (Perhaps it is
correct, but I don't know anyone that knows if.)

Instead of fixing the bug I have re-derived the algorithm from the
invariant together with a (now hopefully correct) proof.  The new
algorithm is contained in Dessy:
    http://www.stud.tu-ilmenau.de/~robertw/dessy/fun/
more specifically in the file:
    http://www.stud.tu-ilmenau.de/~robertw/dessy/fun/WeightedTrees.hs

The derivation, proof (and hint to Adam's bug) are in:
    http://www.stud.tu-ilmenau.de/~robertw/dessy/fun/democratic/sequence.hs

(The so-called hedge-union, -intersection, and -difference is also
implemented: function 'x_merge_width' does all three:
    http://www.stud.tu-ilmenau.de/~robertw/dessy/fun/Dessy.hs )

A paper which presents the new (much simpler) algorithm and its proof
putting it in scientific context is in preparation.

Users that prefer proven algorithms over tested ones are free to use
my implementation instead of the existing ones.  (At moment, there is
no proven and tested implementation.  Of course this will change
soon.)

As for the maintenance of Data.FiniteMap and DData.Map, I don't know
whether it is worth "fixing" the implementations or one would better
replace them by a completely new design.  Anyway, algorithms have no
copyright and everyone is free to use the new "weight-balancer
according to Will" to implement his own data structures.  Oh, by the
way, some of the other balancers in Dessy (or DData) might be more
efficient than weight-based balancing anyway, I'll make some
measurements later this year.

good time,
Bob