Hello libraries and cafe, We (Hirai and I) would like to tell you our paper relating to Data.Set and Data.Map. "Balancing Weight-Balanced Trees" is now accepted and will appear in Journal of Functional Programming. The camera-ready version of the paper is available from: http://www.mew.org/~kazu/proj/weight-balanced-tree/ Please recall that Taylor Campbell reported a bug of Data.Map in last Summer. In some cases, the balance of Data.Map is broken after delete operations. This triggered our research. http://article.gmane.org/gmane.comp.lang.haskell.libraries/13444 Though Data.Set/Data.Map are based of a variant Weight-Balanced tree by Adams, we target the original Weight-Balanced tree by Nievergelt and Reingold. They are parameterized algorithms and the difference of two algorithms is quite small. But the original has smaller conditions which are gentle for proof. We identified the valid area of two parameters of the original Weight-Balanced tree and showed <3,2> is only one integer solution. Soundness is proved in Coq and completeness is verified with four algorithms to generate counterexamples for the outside of the valid area. "wttree.scm" of MIT/GNU Scheme and slib have already incorporated our fixes. When I offered our fixes to MIT/GNU Scheme, Taylor Campbell appeared again. I understand that he is an MIT/GNU Scheme guy and found the bug of Data.Map when re-implementing "wttree.scm" consulting Data.Map. :-) We think it's Haskell community turn now. Data.Set/Data.Map are still based on the variant whose soundness is not proved yet. If interested, let's discuss whether or not we should replace the variant with the original in Data.Set/Data.Map. We guess that Milan Straka, a big contributer of the container package, has his opinion. We welcome opinions from other people, two. Regards, --Kazu