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)