3
\$\begingroup\$

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)
\$\endgroup\$
2
\$\begingroup\$

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.

\$\endgroup\$
  • \$\begingroup\$ Isn't access to the item in a Tree via skewData not O(1) anymore, but linear with tree depth, now? I have considered lens but I'm not foo familiar with it. I love the idea of deriving Functor and Ord, that seems to clean up a lot! \$\endgroup\$ – WorldSEnder Jun 30 '18 at 21:43
  • \$\begingroup\$ I don't follow, skewData is now \(Tree a _) -> a. \$\endgroup\$ – Gurkenglas Jun 30 '18 at 21:45
  • \$\begingroup\$ Ah yes, missed that. It really decomposes nicely. \$\endgroup\$ – WorldSEnder Jun 30 '18 at 21:46
  • \$\begingroup\$ A quick look over the last file tells me there's more to improve, but I think I'll have you shrink that file down using this change first. \$\endgroup\$ – Gurkenglas Jun 30 '18 at 22:32

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.