trjhtr

I implemented the Brodal heap from Brodal & Osaki 1996: Optimal Purely Functional Priority Queues in haskell. The paper gives an implementation in ML but without higher-kinded types. The goal was to introduce some more type-safety by tagging the types Heap and SkewBinomialTree with their ranks. I am aware that an implementation already exists in the package heaps.

The implementation is split into three parts. Data.FunctionalHeap implements the main interface and depends on Data.FunctionalHeap.SkewBinomialTree which implements only SkewBinomialTrees and Data.FunctionalHeap.Internal.Constraints which offers support to teach Haskell the semantics of "ranks".

My main concern is readability and functionality. As this is one of my first Haskell projects, I'd also appreciate feedback about the project layout and interface and getting rid of unneeded dependencies.

dependencies:
- base >= 4.7 && < 5
- constraints >= 0.10
- typelits-witnesses >= 0.3.0.0
- ghc-typelits-natnormalise >= 0.6.1

// Data.FunctionalHeap.Internal.Constraints
-# LANGUAGE ConstraintKinds #-
-# LANGUAGE DataKinds #-
-# LANGUAGE FlexibleInstances #-
-# LANGUAGE GADTs #-
-# LANGUAGE KindSignatures #-
-# LANGUAGE MultiParamTypeClasses #-
-# LANGUAGE RankNTypes #-
-# LANGUAGE TypeOperators #-
-# LANGUAGE TypeFamilies #-
-# LANGUAGE TypeInType #-

module Data.FunctionalHeap.Internal.Constraints(
 Rank,
 KnownRank,
 CmpRank,
 lessImpliesLessEqForP1,
 zeroIsSmallest,
 monotonicNat,
 reflexiveRank,
 decreasingNat,
 monotonicRank,
 LessOrMore,
 type (<),
 type (<=),
 (<&>>),
 (<&->)
) where

import Data.Constraint (type (:-)( Sub ), Dict( Dict ), withDict, mapDict)
import Data.Type.Bool (type (||))
import Data.Type.Equality (type (==))
import Data.Ord (Ordering)
import GHC.TypeLits (Nat, KnownNat, CmpNat, type (+))
import Unsafe.Coerce (unsafeCoerce)

infixr 0 <&-> -- use dict in expression
infixl 1 <&>> -- basically modus ponens

-- Given a dict, derive something that needs its contents (without ugly mattern matching)
(<&->) :: Dict a -> (a => r) -> r
(<&->) = withDict
-- Given a dict, apply an entailment to the dict
(<&>>) :: Dict a -> a :- b -> Dict b
(<&>>) = flip mapDict


type Rank = Maybe Nat

class KnownRank (r :: Rank) where
-- rankSing :: Maybe Integer

instance KnownNat n => KnownRank (Just n) where
-- rankSing = Just (natVal (Proxy :: Proxy n))

instance KnownRank Nothing where
-- rankSing = Nothing

type family CmpRank (l :: Rank) (r :: Rank) :: Ordering where
 CmpRank Nothing Nothing = EQ
 CmpRank (Just n) Nothing = LT
 CmpRank Nothing (Just n) = GT
 CmpRank (Just l) (Just r) = CmpNat l r

infix 4 <, <=
type x < y = CmpRank x y ~ LT
type x <= y = (CmpRank x y == LT || CmpRank x y == EQ) ~ True

class (KnownRank d', d <= d') => LessOrMore d d' where
instance (KnownRank d', d <= d') => LessOrMore d d' where

axiom :: forall a. Dict a -- Please don't hurt me
axiom = unsafeCoerce (Dict :: Dict (a ~ a))

lessImpliesLessEqForP1 :: forall d e. (KnownNat d, KnownRank e, Just d < e) :- (Just (d + 1) <= e)
lessImpliesLessEqForP1 = Sub axiom

zeroIsSmallest :: forall d. (KnownRank d) :- (Just 0 <= d)
zeroIsSmallest = Sub axiom

monotonicNat :: forall d. (KnownNat d) :- (KnownNat (d + 1))
monotonicNat = Sub axiom

reflexiveRank :: forall d. (KnownRank d) :- (d <= d)
reflexiveRank = Sub axiom

decreasingNat :: forall d e. (KnownNat d, KnownRank e, (Just (d + 1)) <= e) :- (Just d < e)
decreasingNat = Sub axiom

monotonicRank :: forall d e f. (KnownNat d, KnownRank e, KnownRank f, Just d < e, e <= f) :- (Just d < f)
monotonicRank = Sub axiom

// Data.FunctionalHeap.SkewBinomialTree
-# LANGUAGE DataKinds #-
-# LANGUAGE GADTs #-
-# LANGUAGE ScopedTypeVariables #-
-# LANGUAGE KindSignatures #-
-# LANGUAGE NamedFieldPuns #-
-# LANGUAGE TypeOperators #-
-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-

module Data.FunctionalHeap.SkewBinomialTree(
 SkewBinomialTree,
 SkewBinomialLayer(..),
 skewData,
 skewLayer,
 singleTree,
 combineTree,
 combineTree'
) where

import GHC.TypeLits (Nat, KnownNat, type (+))
import Data.Kind (Type)

-- Layer 0 = 
-- Layer (d + 1) = Layer d + [Tree d] (binomial link)
-- Layer (d + 1) = Tree d + Tree d (skew type A)
-- Layer (d + 1) = [Tree 0] + Layer d + [Tree d]

-- Tree d = a x Layer d
data SkewBinomialLayer :: Type -> Nat -> Type where
 Layer0 :: SkewBinomialLayer a 0
 BinomialLayer :: KnownNat d => 
 lowerLayer_ :: SkewBinomialLayer a d,
 linkedTree_ :: SkewBinomialTree a d
 -> SkewBinomialLayer a (d + 1)
 SkewALayer :: KnownNat d => 
 leftTree_ :: SkewBinomialTree a d,
 rightTree_ :: SkewBinomialTree a d
 -> SkewBinomialLayer a (d + 1)
 SkewBLayer :: KnownNat d => 
 singleTree_ :: SkewBinomialTree a 0,
 lowerLayer_ :: SkewBinomialLayer a d,
 linkedTree_ :: SkewBinomialTree a d
 -> SkewBinomialLayer a (d + 1)

data SkewBinomialTree :: Type -> Nat -> Type where
 SkewBinomialTree :: 
 data_ :: a,
 layer_ :: SkewBinomialLayer a d
 -> SkewBinomialTree a d

singleTree :: a -> SkewBinomialTree a 0
singleTree el = SkewBinomialTree data_ = el, layer_ = Layer0 

combineTree :: (Ord a, KnownNat d)
 => SkewBinomialTree a d -> SkewBinomialTree a d -> a -> SkewBinomialTree a (d + 1)
combineTree t1 t2 el =
 let d1 = data_ t1
 d2 = data_ t2
 in case (d1 < el, d2 < el, d1 < d2)
 -- d1 >= el && d2 >= el
 of (False, False, _) -> SkewBinomialTree 
 data_ = el,
 layer_ = SkewALayer 
 rightTree_ = t1,
 leftTree_ = t2
 
 
 -- d1 < el || d2 < el && d1 < d2
 (_, _, True) -> SkewBinomialTree 
 data_ = d1,
 layer_ = SkewBLayer 
 singleTree_ = singleTree el,
 lowerLayer_ = layer_ t1,
 linkedTree_ = t2
 
 
 -- d1 < el || d2 < el && d1 >= d2
 (_, _, False) -> SkewBinomialTree 
 data_ = d2,
 layer_ = SkewBLayer 
 singleTree_ = singleTree el,
 lowerLayer_ = layer_ t2,
 linkedTree_ = t1
 
 

combineTree' :: (Ord a, KnownNat d)
 => SkewBinomialTree a d -> SkewBinomialTree a d -> SkewBinomialTree a (d + 1)
combineTree' left right =
 let d1 = data_ left
 d2 = data_ right
 in case d1 < d2
 of True -> SkewBinomialTree 
 data_ = d1,
 layer_ = BinomialLayer 
 lowerLayer_ = layer_ left,
 linkedTree_ = right
 
 
 _ -> SkewBinomialTree 
 data_ = d2,
 layer_ = BinomialLayer 
 lowerLayer_ = layer_ right,
 linkedTree_ = left
 
 

skewData :: SkewBinomialTree a d -> a
skewData = data_

skewLayer :: SkewBinomialTree a d -> SkewBinomialLayer a d
skewLayer = layer_

// Data.FunctionalHeap
-# LANGUAGE ConstraintKinds #-
-# LANGUAGE DataKinds #-
-# LANGUAGE FlexibleInstances #-
-# LANGUAGE GADTs #-
-# LANGUAGE ScopedTypeVariables #-
-# LANGUAGE KindSignatures #-
-# LANGUAGE NamedFieldPuns #-
-# LANGUAGE RankNTypes #-
-# LANGUAGE TypeApplications #-
-# LANGUAGE TypeOperators #-
-# LANGUAGE TypeFamilies #-
-# LANGUAGE TypeInType #-

module Data.FunctionalHeap(
 Heap(..),
 BootstrappedHeap(..),
 BrodalHeap(..),
) where

import Data.Constraint (Dict( Dict ))
import Data.FunctionalHeap.Internal.Constraints
import Data.FunctionalHeap.SkewBinomialTree (SkewBinomialTree, SkewBinomialLayer(..), combineTree, combineTree', singleTree, skewData, skewLayer)
import Data.Kind (Type, Constraint)
import Data.Typeable ((:~:)( Refl ))
import Data.Ord (compare)
import Data.Proxy (Proxy(..))
import GHC.TypeLits (Nat, KnownNat, sameNat, CmpNat, type (+))
import GHC.TypeLits.Compare (cmpNat, SCmpNat(..))

data SizedHeap (d :: Rank) a where
 EmptyHeap :: SizedHeap Nothing a
 TrailingHeap :: forall a d e. (KnownNat d, KnownRank e, Just d < e)
 => SkewBinomialTree a d -> SizedHeap e a -> SizedHeap (Just d) a
 -- must either have a trailing or empty heap after
 -- both trees must have same order
 LeadingHeap :: forall a d e. (KnownNat d, KnownRank e, Just d < e)
 => SkewBinomialTree a d -> SkewBinomialTree a d -> SizedHeap e a -> SizedHeap (Just d) a

data CSizedHeap (c :: Rank -> Constraint) a where
 CSizedHeap :: forall a c d. c d => SizedHeap d a -> CSizedHeap c a

consumeCSizedHeap :: (forall d. c d => SizedHeap d a -> r) -> CSizedHeap c a -> r
consumeCSizedHeap f (CSizedHeap heap) = f heap

useCSizedHeap :: CSizedHeap c a -> (forall d. c d => SizedHeap d a -> r) -> r
useCSizedHeap heap f = consumeCSizedHeap f heap

data CSkewBinomialTree (c :: Nat -> Constraint) a where
 CSkewBinomialTree :: forall a c d. c d => SkewBinomialTree a d -> CSkewBinomialTree c a

consumeCSizedTree :: (forall d. c d => SkewBinomialTree a d -> r) -> CSkewBinomialTree c a -> r
consumeCSizedTree f (CSkewBinomialTree tree) = f tree

useCSizedTree :: CSkewBinomialTree c a -> (forall d. c d => SkewBinomialTree a d -> r) -> r
useCSizedTree tree f = consumeCSizedTree f tree

insertToSized :: (KnownNat d, KnownRank e, Just d <= e)
 => SkewBinomialTree a d -> SizedHeap e a -> SizedHeap (Just d) a
insertToSized smallTree EmptyHeap = TrailingHeap smallTree EmptyHeap
insertToSized (smallTree :: SkewBinomialTree a d) heap@(TrailingHeap (leadingTree :: SkewBinomialTree a e) trailingHeap) =
 case cmpNat (Proxy :: Proxy d) (Proxy :: Proxy e)
 of CLT Refl -> TrailingHeap smallTree heap
 CEQ _ Refl -> LeadingHeap smallTree leadingTree trailingHeap
 _ -> error "Impossible branch"
insertToSized (smallTree :: SkewBinomialTree a d) (LeadingHeap _ _ _) = error "Can't insert here"

addToSized :: forall a d. (KnownRank d, Ord a)
 => SizedHeap d a -> a -> CSizedHeap KnownRank a
addToSized EmptyHeap el = CSizedHeap $ TrailingHeap (singleTree el) EmptyHeap
addToSized heap@(TrailingHeap _ _) el =
 Dict <&>> zeroIsSmallest @d <&->
 CSizedHeap $ insertToSized (singleTree el) heap
addToSized (LeadingHeap (t1 :: SkewBinomialTree a d') t2 (trailingHeap :: SizedHeap e a)) el =
 Dict <&>> lessImpliesLessEqForP1 @d' @e <&->
 Dict <&>> monotonicNat @d' <&->
 CSizedHeap $ insertToSized (combineTree t1 t2 el) trailingHeap

-- Makes sure that heap is not a LeadingHeap by combining
prepareMeldSized :: forall a d. (KnownRank d, Ord a)
 => SizedHeap d a -> CSizedHeap (KnownRank -, d <= d'-) a
prepareMeldSized (LeadingHeap (t1 :: SkewBinomialTree a d') t2 (tail :: SizedHeap e a)) =
 Dict <&>> lessImpliesLessEqForP1 @d' @e <&->
 Dict <&>> monotonicNat @d' <&->
 prepareMeldSized $ insertToSized (combineTree' t1 t2) tail
prepareMeldSized heap =
 --Dict <&>> reflexiveRank @e <&->
 CSizedHeap heap

-- TODO: use insertToSized instead??
insSized :: forall a e d. (KnownNat d, KnownRank e-, (Just d) <= e-, Ord a)
 => SkewBinomialTree a d -> SizedHeap e a -> CSizedHeap KnownRank a
insSized tree EmptyHeap =
 CSizedHeap $ TrailingHeap tree EmptyHeap
insSized tree heap@(TrailingHeap (leading :: SkewBinomialTree a e') (tail :: SizedHeap f a)) =
 -(Dict :: Dict (KnownNat e, KnownRank f, (Just e) < f)) <&>> lessImpliesLessEqForP1 <&->-
 Dict <&>> monotonicNat @e' <&->
 case cmpNat (Proxy :: Proxy d) (Proxy :: Proxy e')
 of CLT Refl -> CSizedHeap (TrailingHeap tree heap)
 CEQ _ Refl -> insSized (combineTree' tree leading) tail
 _ -> error "Illegal branch"

meldSized :: forall a d e. (KnownRank d, KnownRank e, Ord a)
 => SizedHeap d a -> SizedHeap e a -> CSizedHeap KnownRank a
meldSized t1 t2 =
 let prepared1 = prepareMeldSized t1
 prepared2 = prepareMeldSized t2
 in consumeCSizedHeap (consumeCSizedHeap meldSized' prepared1) prepared2

meldSized' :: (KnownRank d, KnownRank e, Ord a)
 => SizedHeap d a -> SizedHeap e a -> CSizedHeap KnownRank a
meldSized' EmptyHeap heap = CSizedHeap heap
meldSized' heap EmptyHeap = CSizedHeap heap
meldSized' heapL@(TrailingHeap (tL :: SkewBinomialTree a d') tailL) heapR@(TrailingHeap (tR :: SkewBinomialTree a e') tailR) =
 Dict <&>> monotonicNat @d' <&->
 case cmpNat (Proxy :: Proxy d') (Proxy :: Proxy e')
 of CLT Refl -> consumeCSizedHeap (insSized tL) $ meldSized' tailL heapR
 CGT Refl -> consumeCSizedHeap (insSized tR) $ meldSized' heapL tailR
 CEQ _ Refl -> consumeCSizedHeap (insSized $ combineTree' tL tR) $ meldSized' tailL tailR

splitLayer :: (KnownNat d)
 => SkewBinomialLayer a d -> (CSizedHeap KnownRank a, [a])
splitLayer = splitLayer' EmptyHeap

splitLayer' :: forall a d e. (KnownNat d, KnownRank e, Just d <= e)
 => SizedHeap e a -> SkewBinomialLayer a d -> (CSizedHeap KnownRank a, [a])
splitLayer' heap Layer0 = (CSizedHeap heap, )
splitLayer' heap (BinomialLayer (lowerLayer_ :: SkewBinomialLayer a d') linkedTree_) =
 Dict <&>> decreasingNat @d' @e <&->
 splitLayer' (TrailingHeap linkedTree_ heap) lowerLayer_
splitLayer' heap (SkewALayer (left :: SkewBinomialTree a d') right) =
 Dict <&>> decreasingNat @d' @e <&->
 (CSizedHeap (LeadingHeap left right heap), )
splitLayer' heap (SkewBLayer single (lower :: SkewBinomialLayer a d') linked) =
 let (heap', list) =
 Dict <&>> decreasingNat @d' @e <&->
 splitLayer' (TrailingHeap linked heap) lower
 in (heap', skewData single : list)

splitMinTreeSized :: forall a d. (KnownRank d, Ord a)
 => SizedHeap d a -> (CSizedHeap (LessOrMore d) a, CSkewBinomialTree KnownNat a)
splitMinTreeSized EmptyHeap = error "Can't split empty heap"
splitMinTreeSized (TrailingHeap tree EmptyHeap) = (CSizedHeap EmptyHeap, CSkewBinomialTree tree)
splitMinTreeSized (TrailingHeap (tree :: SkewBinomialTree a d') (tail :: SizedHeap e a)) =
 let (trailHeap, trailMinTree) = splitMinTreeSized tail
 trailMin = useCSizedTree trailMinTree skewData
 in if trailMin < skewData tree
 then (useCSizedHeap trailHeap (
 (trail :: SizedHeap f a) -> Dict <&>> monotonicRank @d' @e @f <&->
 CSizedHeap $ TrailingHeap tree trail), trailMinTree)
 else (CSizedHeap tail, CSkewBinomialTree tree)
splitMinTreeSized (LeadingHeap t1 t2 EmptyHeap) =
 if skewData t1 < skewData t2
 then (CSizedHeap $ TrailingHeap t2 EmptyHeap, CSkewBinomialTree t1)
 else (CSizedHeap $ TrailingHeap t1 EmptyHeap, CSkewBinomialTree t2)
splitMinTreeSized (LeadingHeap (t1 :: SkewBinomialTree a d') t2 (tail :: SizedHeap e a)) =
 let (trailHeap, trailMinTree) = splitMinTreeSized tail
 trailMin = useCSizedTree trailMinTree skewData
 in case (trailMin < skewData t1, trailMin < skewData t2)
 of (False, _) -> (CSizedHeap (TrailingHeap t2 tail), CSkewBinomialTree t1)
 (_, False) -> (CSizedHeap (TrailingHeap t1 tail), CSkewBinomialTree t2)
 _ -> (useCSizedHeap trailHeap (
 (trail :: SizedHeap f a) -> Dict <&>> monotonicRank @d' @e @f <&->
 CSizedHeap $ LeadingHeap t1 t2 trail), trailMinTree)

deleteMinSized :: (KnownRank d, Ord a)
 => SizedHeap d a -> (a, CSizedHeap KnownRank a)
deleteMinSized EmptyHeap = error "Can't delete from empty heap"
deleteMinSized heap =
 let (heap', minTree) = splitMinTreeSized heap
 (heap'', rest) = useCSizedTree minTree (splitLayer . skewLayer)
 meldedheap = consumeCSizedHeap (consumeCSizedHeap meldSized heap') heap''
 newheap = foldl (consumeCSizedHeap addToSized) meldedheap rest
 in (useCSizedTree minTree skewData, newheap)

instance Foldable (SizedHeap e) where
 foldMap f EmptyHeap = mempty
 foldMap f (TrailingHeap head tail) = f (skewData head) `mappend` foldMap f tail
 foldMap f (LeadingHeap t1 t2 tail) = f (skewData t1) `mappend` f (skewData t2) `mappend` foldMap f tail

class Heap (a :: Type -> Type) where
 empty :: a t
 isEmpty :: a t -> Bool

 insert :: Ord t => a t -> t -> a t

 meld :: Ord t => a t -> a t -> a t

 findMin :: Ord t => a t -> t
 findMin h = fst $ removeMin h

 removeMin :: Ord t => a t -> (t, a t)

instance Heap (CSizedHeap KnownRank) where
 empty = CSizedHeap EmptyHeap
 isEmpty (CSizedHeap EmptyHeap) = True
 isEmpty _ = False
 insert (CSizedHeap heap) = addToSized heap
 meld (CSizedHeap heapL) (CSizedHeap heapR) = meldSized heapL heapR
 findMin (CSizedHeap heap) = minimum heap
 removeMin (CSizedHeap heap) = deleteMinSized heap

data Heap h => RBstHeap h a = RBstHeap 
 root_ :: a,
 queue_ :: h (RBstHeap h a)


instance (Heap h, Ord a) => Ord (RBstHeap h a) where
 compare left right = compare (root_ left) (root_ right)
instance (Heap h, Eq a) => Eq (RBstHeap h a) where
 left == right = root_ left == root_ right

data Heap h => BootstrappedHeap h a = Empty | BootstrappedHeap underlying_ :: RBstHeap h a 

instance Heap h => Heap (BootstrappedHeap h) where
 empty = Empty
 isEmpty Empty = True
 isEmpty _ = False

 insert h x = meld h BootstrappedHeap underlying_ = RBstHeap root_ = x, queue_ = empty 

 meld Empty r = r
 meld l Empty = l
 meld BootstrappedHeapunderlying_=left BootstrappedHeapunderlying_=right =
 let xl = root_ left
 xr = root_ right
 ql = queue_ left
 qr = queue_ right
 in if root_ left < root_ right
 then BootstrappedHeap underlying_ = RBstHeap root_ = xl, queue_ = insert ql right 
 else BootstrappedHeap underlying_ = RBstHeap root_ = xr, queue_ = insert qr left 

 findMin = root_ . underlying_

 removeMin BootstrappedHeapunderlying_ =
 if isEmpty $ queue_ underlying_
 then (root_ underlying_, Empty)
 else let (RBstHeaproot_=newmin, queue_=q1, q2) = removeMin $ queue_ underlying_
 in (root_ underlying_, BootstrappedHeap underlying_ = RBstHeap root_ = newmin, queue_ = meld q1 q2 )

type BrodalHeap = BootstrappedHeap (CSizedHeap KnownRank)

Field names need not indicate types, a good IDE makes that information available. Replace singleTree_ in SkewBLayer with the simpler el. SkewBinomialLayer decomposes:

data Layer f d where
 Layer0 :: Layer 0
 Layer :: KnownNat d => f (Layer f d) -> Layer f (d + 1)

data SkewBinomial a l
 = SkewA left_ :: Tree a l, right_ :: Tree a l 
 | SkewB single_ :: a, linked_ :: Tree a l, lower_ :: l 
 | Binomial linked_ :: Tree a l, lower_ :: l 

data Tree a l = Tree a l deriving Functor
instance Ord a => Ord (Tree a l) where compare = comparing skewData

type SkewBinomialLayer a = Layer (SkewBinomial a)

combineTree t1 t2 el = min (Tree el $ Layer $ SkewA t2 t1) $
 let [small, big] = sort [t1, t2] in fmap (Layer . SkewB el big) small

combineTree' t1 t2 =
 let [small, big] = sort [t1, t2] in fmap (Layer . Binomial big) small

Consider lens.