[Haskell-cafe] \Statically checked binomail heaps?
Maciej Kotowicz
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.
_______________________________________________
Haskell-Cafe mailing list
Haskel...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Wouter Swierstra
> 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.
Okasaki, C. DR EECS
enforce the shape invariants. I dug up an old email from 1998 talking
about how to do this with nested types, and posted it to my blog:
http://okasaki.blogspot.com/2009/10/binomial-queues-as-nested-type.html
-- Chris
Bertram Felgenhauer
> 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)