[Haskell-cafe] \Statically checked binomail heaps?
Maciej Kotowicz
kotowicz.maciej at gmail.com
Sun Oct 18 06:49:49 EDT 2009
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.
More information about the Haskell-Cafe
mailing list