[Haskell-cafe] \Statically checked binomail heaps?

[Bertram Felgenhauer]

Maciej Kotowicz wrote:
> I'm trying to implement a binomial heaps from okaski's book [1]
> but as most it's possible to be statically checked for correctness of
> definition.

How about this encoding in Haskell 98?

    data Tree a t = Tree { root :: a, children :: t }
    data Nest a t = Nest { head :: Tree a t, tail :: t }

where
- Tree a () is a binomial tree of order 0
- Tree a (Nest a ()) is a binomial tree of order 1
- Tree a (Nest a (Nest a ())) is a binomial tree of order 2. and so on

    data Heap' a t
        = Z'
        | D0' (Heap' a (Nest a t))
        | D1' (Heap' a (Nest a t)) (Tree a t)

With (Tree a t) representing a binomial tree of rank n,
- Heap' a t  represents the list of binomial trees of rank >= n in a heap
- Z'         represents an empty list
- D0' xs     represents a list /without/ a tree of rank n
- D1' xs x   represents a list /with/ a tree of rank n, namely x.

Finally, define

    type Heap a = Heap' a ()

This forces Heap to be a well-shaped binomial heap, up to the equality
D0' Z' = Z'.

The main difference to "standard" binomial heaps is the existence of the
D0' nodes which represent skipped ranks. This makes the type checking
much easier (no comparison of natural numbers is required). It also
makes rank calculations unecessary - the rank increases implicitely as
the heap is traversed.

Heap order can be maintained by using a smart constructor:

    -- combine two binomial trees of rank n into one of rank n+1
    mkTree' :: Ord a => Tree a t -> Tree a t -> Tree a (Nest a t)
    mkTree' l@(Tree a x) r@(Tree b y)
        | a < b = Tree a (Nest r x)
        | True  = Tree b (Nest l y)

Here is insert, as an example of a non-trivial operation:

    insert' :: Ord a => Heap' a t -> Tree a t -> Heap' a t
    insert' Z'        b = D1' Z' b
    insert' (D0' x)   b = D1' x b
    insert' (D1' x a) b = D0' (x `insert'` mkTree' a b)

HTH,

Bertram

P.S. As a refinement, one can define
    data Heap a = Z | D0 | D1 (Heap' a a) a

This improves memory efficiency at the cost of requiring more code, like

    mkTree :: Ord a => a -> a -> Tree a a
    mkTree a b | a < b = Tree a b
               | True  = Tree b a

    insert :: Ord a => Heap a -> a -> Heap a
    insert Z        b = D1 Z' b
    insert (D0 x)   b = D1 x b
    insert (D1 x a) b = D0 (x `insert'` mkTree a b)