Refactored version of Okasaki's skew-binomial heaps in Standard ML

In his book, Purely Functional Data Structures, Chris Okasaki provides an implementation of skew-binomial heaps (p. 137). Unfortunately, the book isn't (legally) freely available anywhere, but his thesis contains another implementation of skew-binomial heaps (p. 83) that only differs in minor inessential ways.

I refactored Okasaki's code with three main goals:

My code is available here. It depends on:

I will split my code so that each part is immediately followed by its explanation.

functor SkewBinHeap (E : HEAP_ENTRY) :> HEAP where type E.key = E.key =
struct
structure E = E
structure R = OrdExtras (struct
type key = int
val compare = Int.compare
end)

datatype α tree = T of α * α list * α tree list

fun root (T (x, _, _)) = #1 x

Okasaki defines a skew-binomial tree of rank r to consist of:

• A root entry
• A list of no more than r auxiliary entries
• A list of child trees of all smaller ranks, in decreasing order

Aside: Okasaki annotates all trees, including children, with their rank. I only annotate top-level trees, which saves some space, but doesn't change the asymptotic bounds of any operation.

datatype α heap = Nil | Cons of int * α E.entry tree * α heap

val empty = Nil

A skew-binomial forest of rank r may be:

• Empty, in which case r is infinity.
• Strict, in which case it consists of:
• A skew-binomial tree of rank r
• A non-relaxed skew-binomial forest of rank greater than r
• Relaxed, in which case it consists of:
• A skew-binomial tree of rank r
• A strict skew-binomial forest of rank r

Aside: Okasaki's original definition neither distinguishes between empty, strict and relaxed forests, nor assigns them ranks. The increased precision of my definition will turn out to be useful.

fun link (Cons (p, u, Cons (q, v, ts))) =
if p = q then
let val (T (x, xs, us), u) = E.reorder root (u, v)
in Cons (1 + p, T (x, xs, u :: us), ts) end
else
Nil
| link _ = Nil

link takes a forest as argument. If the forest is relaxed and of rank r, link returns an equivalent (possibly still relaxed) forest of rank r+1. Otherwise, link returns the empty forest.

fun cons (x, ts) =
case link ts of
Nil => Cons (0, T (x, nil, nil), ts)
| Cons (r, T (y, xs, us), ts) =>
let val (x, y) = E.reorder #1 (x, y)
in Cons (r, T (x, y :: xs, us), ts) end

cons (called insert in Okasaki's book) inserts a single element into a forest. If the forest is relaxed, cons skew-links the forest's first two trees with the new element. Otherwise, cons inserts a singleton tree of rank 0 at the front of the forest.

fun strict ts = case link ts of Nil => ts | ts => strict ts

strict (called normalize in Okasaki's book) turns a forest into an equivalent non-relaxed one, by repeatedly calling link.

Observation: It's very convenient that link distinguishes between relaxed and non-relaxed forests. This way, I don't need to reimplement the same distinction in cons and strict.

Question: Does the convenience of using link outweigh the unnaturality in how it handles strict forests?

fun concat (ts, Nil) = ts
| concat (Nil, ts) = ts
| concat (Cons ts, Cons us) =
let val ((r, t, ts), us) = R.reorder #1 (ts, us)
in Cons (r, t, strict (concat (ts, Cons us))) end

concat (called merge in Okasaki's book) combines two forests into a single one with the elements of both.

fun extract ts =
case other ts of
Nil => ts
| Cons us => #1 (E.reorder (root o #2) (ts, us))

and other (p, u, Cons ts) =
let val (q, v, ts) = extract ts
in Cons (q, v, Cons (p, u, ts)) end
| other _ = Nil

extract (called removeMinTree in Okasaki's book) takes a nonempty forest, and moves the tree with the smallest root to the front.

fun relabel (_, nil, us) = us
| relabel (r, t :: ts, us) =
let val r = r - 1 in relabel (r, ts, Cons (r, t, us)) end

fun rebuild (r, T (x, xs, ts), us) =
(x, foldl cons (concat (relabel (r, ts, Nil), us)) xs)

rebuild reinserts the auxiliary entries and children of the removed tree (see extract above) back into the forest. The root of the removed tree is returned as a separate result.

Observation: The expression foldl cons (concat (relabel (r, ts, Nil), us)) xs is... a little bit too long.

Question: Should I split it? For example:

fun rebuild (r, T (x, xs, ts), us) =
let
val ts = relabel (r, ts, Nil)
val ts = concat (ts, us)
in
(x, foldl cons ts xs)
end

fun uncons Nil = NONE
| uncons (Cons ts) = SOME (Lazy.delay (rebuild o extract) ts)
end

uncons (called isEmpty, findMin and deleteMin in Okasaki's book) determines whether the tree is empty. If it is not, the smallest entry may be removed, if the user forces a suspension.