[Haskell-cafe] \Statically checked binomail heaps?

[Maciej Kotowicz]

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.