While working on AVL for teaching I found an alternative to the AVL that seems overall better than the current ocaml implementation. The code is available here: https://github.com/craff/ocaml-avl/tree/master. The Readme.md contains the inequality needed to prove correctness and termination of the balancing function “join”.
slightly simpler code or at least not more complicated (see below)
seems faster in many cases (not always and strangely depends on compilation options). Use dune exec --release ./test.exe for some simple tests. dune exec ./test.exe give slightly less favorable result for the mem function which is unchanged?
Before submitting a PR, I think it could be a good idea to call for comments here.
I added a copy of set.ml[i] as oriset.ml[i] to make sure we compare with the same compilation options. It is strange we have to do that: stlib are not compiled with dune --release by default ?
The timings are now more natural: trees are a bit better balanced (I thought the opposite, but checked): adding and union is between 0-15% faster,
searching is between 5% faster and 10% slower, which is hard to explain with better balanced tree and the same mem function. remove is between 15% faster to 25% slower.
Here are the detailled timings:
Adding 300000 consecutive integers in a set:
OCaml’s set: : 0.15294s, branches: (min: 18, max: 20, avg: 18.3)
Proposal set: : 0.12244s, branches: (min: 18, max: 19, avg: 18.3)
ordered add -19.95%
Checking mem on all elements of the above:
OCaml’s set: : 0.01537s
Proposal set: : 0.01510s
check mem -1.76%
Removing all elements of the above:
OCaml’s set: : 0.01496s
Proposal set: : 0.01785s
ordered rm 19.38%
Adding 300000 random integers in a set:
OCaml’s set: : 0.26909s, branches: (min: 13, max: 24, avg: 18.9)
Proposal set: : 0.25805s, branches: (min: 14, max: 23, avg: 18.5)
random add -4.10%
Checking mem on all elements of the above:
OCaml’s set: : 0.02064s
Proposal set: : 0.02147s
check mem 4.00%
Removing all elements of the above:
OCaml’s set: : 0.02834s
Proposal set: : 0.02190s
random rm -22.72%
Building set of ~300000 elements by random union:
OCaml’s set: : 0.20277s, branches: (min: 11, max: 26, avg: 19.4)
Proposal set: : 0.18332s, branches: (min: 14, max: 22, avg: 18.6)
random union -9.59%
Checking mem on all elements of the above:
OCaml’s set: : 0.01679s
Proposal set: : 0.01831s
check mem 9.07%
Removing all elements of the above:
OCaml’s set: : 0.02493s
Proposal set: : 0.02008s
random union rm -19.46%
Thanks for the pointer, I came on the discussion and also improved the code on github (there was still some bugs… which I fixed by writting a paper proof available here. I might attempts a formal proof later).
An advantage of storing the size on all nodes, is that it is possible to provide O(log n) time functions
val locate : key -> 'a t -> bool * int
(** [locate k m] is a pair [(present, pos)] where [present] is true iff [k]
is bound in [m] and [pos] is the number of keys of [m] preceding [k]. *)
val get : 'a t -> int -> 'a
(** [get i m] is the [i]th value of [m].
@raise Invalid_argument if the index is out of bounds. *)
val get_binding : 'a t -> int -> key * 'a
(** [get_binding m i] is the [i]th binding of [m] according to the key
order. *)
which I find useful for incrementally maintaining sorted HTML lists and tables in JavaScript, since JS provides indexed access and mutation. When you get an incoming element to add, check the expected position and whether it’s present, then insert or update the HTML node at that position, and update the sorted model.
(The above signature is from the Prime_enummap module of the prime library which I didn’t publish in OPAM as there were already many stdlib supplements around. I just ran a benchmark I had lying around, and adding elements is slower than stdlib by 15-20 % and not up to date on the API, so sounds like the current proposal is closer to a candidate for stdlib. My invariant is 4 * min nL nR >= max nL nR where nL and nR are the sizes of the left and right branches.)
There’s an even bigger benefit to this by allowing nodes to store arbitrary monoidal “measures” in each node (as in the Hinze 2-3 finger tree paper*). This generalization opens tree structures to a wealth of different applications. It’s disappointing that most standard libraries do not provide such functionality, but it’s easy enough to build out on your own if you’re willing to build a tree structure from scratch.
* Note that this is mostly applicable to read and “simple” update operations, as operations such as concatenation or subsetting can become arbitrarily expensive depending on the invariants you want to maintain and the exact shape of your tree structure.