Consider a GADT-based implementation

[treeowl]

Instead of a (higher-order) nested type, we could use a GADT to represent a binomial tree. The big potential advantage is that such a representation allows for a more direct approach to deletion:

• Walk down the spine to find the minimum.
• Walk back up to the minimal tree.
• Walk down the subtrees of the minimal tree.
• On the way back up, meld into the original spine, discarding the appropriate tree.

This approach carries as it adds, whereas the current approach (roughly speaking) adds and then propagates carries. I believe it should, therefore, allocate less on the heap. Only benchmarks will tell the whole story, of course.

[treeowl]

I guess another thing that might be worth trying, at least as an experiment, is using unsafeCoerce for the job. That is, instead of building up a function to walk the tree's children, just accumulate a counter. Use unsafeCoerce at every step down the child list to turn rk into Succ rk'. It's pretty evil, but I think it'll at least give us an idea of whether the GADT approach is worth pursuing.

[treeowl]

Hmmmm.... I feel like I'm thinking about this whole carrying problem wrong somehow. Suppose we use a two-pass algorithm: one pass to find the minimal tree and a second to actually extract. How might that second pass look? The spine consists of some number of Skips followed by a mixture of Cons and Skip. The initial segment of Skips will be filled in from some tail of the minimal tree, so we have to do that on the way up. Once we hit a Cons, every further addition will carry, no matter what. Interesting. That first Cons will turn to a Skip. Beyond that point, each Cons will turn to a Cons (which can use its original tree) and each Skip will turn to a Skip. Instead of using the carries as we go, we should be able to accumulate them into a tree, and stick it on the end. Something like that. Can we avoid two full passes? Well, we can surely handle the initial segment of Skips without accumulation, so we should probably do that. Afterwards, imagine sending down a feeler looking for something smaller than the current minimum. Once it finds something, we can walk down to that point before sending out another feeler. We'll typically only double-walk short pieces each time, which should be cheap. We'll only do it in one go if the roots are increasing and then the last one decreases.

[treeowl]

Bleh. I don't think any of these ideas are going anywhere, at least anytime soon.