+{-# LANGUAGE
+ EmptyDataDecls,
+ TypeFamilies,
+ TypeOperators,
+ UndecidableInstances
+ #-}
+module Data.HList.Heap
+ ( Heap
+
+ , Empty
+ , Unit
+ , Insert
+ , Merge
+ , MergeAll
+ , IsEmpty
+ , FindMin
+ , DeleteMin
+ , SplitMin
+ )
+ where
+
+import Data.HList
+import Types.Data.Bool
+import Types.Data.Ord
+
+
+data Empty
+data Node key value heaps
+
+class Heap h
+instance Heap Empty
+instance Heap hs => Heap (Node k v hs)
+
+type Unit k v = Node k v Nil
+
+type family IsEmpty h
+type instance IsEmpty Empty = True
+type instance IsEmpty (Node k v hs) = False
+
+type Insert k v h = Merge (Unit k v) h
+
+type family Merge h1 h2
+type instance Merge h1 Empty = h1
+type instance Merge Empty h2 = h2
+type instance Merge (Node k1 v1 hs1) (Node k2 v2 hs2)
+ = If (k1 :<: k2)
+ (Node k1 v1 (Cons (Node k2 v2 hs2) hs1))
+ (Node k2 v2 (Cons (Node k1 v1 hs1) hs2))
+
+type family MergeAll hs
+type instance MergeAll Nil = Empty
+type instance MergeAll (Cons h Nil) = h
+type instance MergeAll (Cons h (Cons h' hs))
+ = Merge (Merge h h') (MergeAll hs)
+
+type family FindMin h
+type instance FindMin (Node k v hs) = Cons k v
+
+type family DeleteMin h
+type instance DeleteMin Empty = Empty
+type instance DeleteMin (Node k v hs) = MergeAll hs
+
+type family SplitMin h
+type instance SplitMin (Node k v hs) = Cons k (Cons v (MergeAll hs))