Adams' Trees Revisited - Correct and Efficient Implementation


We present a correct proof of Adams' trees of bounded balance, which are used in Haskell to implement Data.Map and Data.Set. Our analysis includes the previously ignored join operation, and also guarantees trees with smaller depth than the original one. Because the Adams' trees can be parametrized, we use benchmarking to find the best choice of parameters. Finally, a saving memory technique based on introducing additional data constructor is evaluated.

The paper was accepted to TFP 2011. The draft paper is available as PDF.

The detailed results of the benchmark are available here. All source code used is available as benchmark.tar.gz.