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 BootstrappedHeap{underlying_=left} BootstrappedHeap{underlying_=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 BootstrappedHeap{underlying_} =
if isEmpty $ queue_ underlying_
then (root_ underlying_, Empty)
else let (RBstHeap{root_=newmin, queue_=q1}, q2) = removeMin $ queue_ underlying_
in (root_ underlying_, BootstrappedHeap { underlying_ = RBstHeap { root_ = newmin, queue_ = meld q1 q2 } })
type BrodalHeap = BootstrappedHeap (CSizedHeap KnownRank)