Hi, first of all this post is literate haskell 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. Remark that binomial heap is list of binomial trees in increasing order of rank and binomial heap of rank r is a node with r child t_1..t_r, where each t_i is binomial tree of rank r - i First I need some langue extension
{-# LANGUAGE TypeFamilies #-} {-# LANGUAGE EmptyDataDecls #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-}
module BinTree where
second type-level Nats and Bools, and Void i some kind of Top for Nats
data Z data S a data Void data True data False
Ok, let define some nice types ;) OrdLList is list of decreasing collections parametrised by type of element and length with is also highest rank of elements plus one, they are heterogeneous by they ranks
type Forest = OrdLList BinTree data OrdLList (t :: * -> * -> * ) a :: * -> * where LNil :: OrdLList t a Z LCons :: t a n -> OrdLList t a n -> OrdLList t a (S n )
Binomial tree is here, a I know i can't check statically an heap property
data BinTree a :: * -> * where Node :: Ord a => a -> Forest a n -> BinTree a n
Heap is very similar to Forest just reversed order
data OrdGList (t :: * -> * -> * ) a :: * -> * where GNil :: OrdGList t a Void GCons :: Lt n m ~ True => t a n -> OrdGList t a m -> OrdGList t a n type Heap a n = OrdGList BinTree a n
Predicate for testing order in Heap
type family Lt a b type instance Lt Z (S a) = True type instance Lt (S a) Z = False type instance Lt (S a) (S b) = Lt a b type instance Lt a Void = True
reflection form type-level nats to Int
class TNum a where toNum :: a -> Int instance TNum Z where toNum _ = 0 instance TNum a => TNum (S a) where toNum _ = 1 + toNum (undefined :: a)
rank of binomial tree
rank :: TNum n => BinTree a n -> Int rank t = toNum $ undefined `asTypeOf` (getN t) getN :: t a n -> n getN _ = undefined :: n
root of binomial trees
root :: BinTree e n -> e root (Node x _ ) = x
And finally first of quite serious function linking two trees with must have the same ranks, giving trees with rank greater by one
link :: Ord a => BinTree a n -> BinTree a n -> BinTree a (S n) link t1@(Node x c1) t2@(Node y c2) | x <= y = Node x $ LCons t2 c1 | otherwise = Node y $ LCons t1 c2
some simple trees for tests
h = GCons t3 $ GCons t GNil t = link t1 t2 t1 = Node 3 LNil t2 = Node 2 LNil t3 = Node 5 LNil
And sadly that's all I can write... for full functionality these data structure should have merge, insert, deleteMin, findMin, defined in [1] as fallow insTree t [] = [t] insTree t ts@(t':ts') | rank t < rank t' = t : ts | otherwise = insTree (link t t') ts' insert x = insTree (Node 0 x []) -- in [1] rank's are write explicit in nodes merge ts [] = ts merge [] ts = ts merge ts1@(t1:ts1') ts2@(t2:ts2') | rank t1 < rank t2 = t1 : merge ts1' ts2 | rank t1 > rank t2 = t2 : merge ts1 ts2' | otherwise = insTree (link t1 t2) $ merge ts1' ts2' removeMinTree [] = error "empty" removeMinTree [t] = (t,[] removeMinTree (t:ts) | root t < root t' = (t,ts) | otherwise = (t',t:ts') where (t',ts') = removeMinTree ts findMin = root . fst . removeMinTree deleteMin ts = merge (rev ts1, ts2) where (Node _ x ts1,ts2) = removeMinTree I try with all this function and with all I have problems with types the types of insTree in my opinion should be sth like: insTree :: (Min n m ~ k,TNum n, TNum m) => BinTree a n -> Heap a m -> Heap a k where Min looks like: type family Min a b type instance Min a Z = Z type instance Min Z a = Z type instance Min (S a) (S b) = S (Min a b) but this won't compile, ghc don't see that k can be the same type as m in first pattern, problems with rest of function was similar exclude removeMinTree with I have no idea what type it should have... Have anyone an idea how make this code working? Any help will be appreciated [1] Purely Functional Data Structures by Chris Okasaki. Cambridge University Press, 1998.