\Statically checked binomail heaps?
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.
Hi Maciej,
insTree t [] = [t] insTree t ts@(t':ts') | rank t < rank t' = t : ts | otherwise = insTree (link t t') ts'
In a way, it's unsurprising that this is where your code breaks. What you're doing here is using a boolean guard to determine where to insert. The problem is that ghc's type checker doesn't learn anything from these boolean guards. In contrast to pattern matching on a GADT, you can always exchange the two branches of an if-than-else without breaking type correctness. To get the code to work the type checker needs learn something about the ranks of t and t' after comparing them.
Have anyone an idea how make this code working?
Use a different language. In particular, you might want to have a look at Agda - a programming language and proof assistand based on dependent types that has a very similar look-and-feel to Haskell. If you're interested, you may want to have a look at similar developments by some of our students at Chalmers: http://web.student.chalmers.se/groups/datx02-dtp/ They've given verified implementations in Agda of some fairly advanced data structures. Hope this helps, Wouter PS - There may be a way around this by writing even more type-level programs in Haskell, basically reflecting (<) on the type-level and doing some really hard work to relate the type level numbers to the value level numbers. Brace yourself for a world of pain.
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)
participants (3)
-
Bertram Felgenhauer -
Maciej Kotowicz -
Wouter Swierstra