module Control.Effect.Helpers.Set (Set(..), Union, Unionable, union, bsort, append, Sort, Sortable,
OrdH(..), Min, Max, Append(..), Split(..),
Nub, Nubable(..),
AsSet, asSet, IsSet,
Subset(..)) where
data Set (n :: [*]) where
Empty :: Set '[]
Ext :: e -> Set s -> Set (e ': s)
asSet :: (Sortable s, Nubable (Sort s)) => Set s -> Set (AsSet s)
asSet x = nub (bsort x)
type AsSet s = Nub (Sort s)
type IsSet s = (s ~ Nub (Sort s))
type SetProperties f = (Union f '[] ~ f, Split f '[] f,
Union '[] f ~ f, Split '[] f f,
Union f f ~ f, Split f f f,
Unionable f '[], Unionable '[] f)
type Union s t = Nub (Sort (Append s t))
union :: (Unionable s t) => Set s -> Set t -> Set (Union s t)
union s t = nub (bsort (append s t))
type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append s t)))
type Sortable s = Bubbler s s
type family Append s t where
Append '[] t = t
Append (x ': xs) ys = x ': (Append xs ys)
append :: Set s -> Set t -> Set (Append s t)
append Empty x = x
append (Ext e xs) ys = Ext e (append xs ys)
type family Nub t where
Nub '[] = '[]
Nub '[e] = '[e]
Nub (e ': e ': s) = Nub (e ': s)
Nub (e ': f ': s) = e ': Nub (f ': s)
class Nubable t where
nub :: Set t -> Set (Nub t)
instance Nubable '[] where
nub Empty = Empty
instance Nubable '[e] where
nub (Ext x Empty) = Ext x Empty
instance (Nub (e ': f ': s) ~ (e ': Nub (f ': s)),
Nubable (f ': s)) => Nubable (e ': f ': s) where
nub (Ext e (Ext f s)) = Ext e (nub (Ext f s))
type Sort l = Bubble l l
bsort :: (Bubbler s s) => Set s -> Set (Sort s)
bsort x = bubble x x
type family Bubble l l' where
Bubble l '[] = l
Bubble l (x ': xs) = Pass (Bubble l xs)
class Bubbler s s' where
bubble :: Set s -> Set s' -> Set (Bubble s s')
instance Bubbler s '[] where
bubble s Empty = s
instance (Bubbler s t, Passer (Bubble s t)) => Bubbler s (e ': t) where
bubble s (Ext _ t) = pass (bubble s t)
type family Pass l where
Pass '[] = '[]
Pass '[e] = '[e]
Pass (e ': f ': s) = Min e f ': (Pass ((Max e f) ': s))
class Passer s where
pass :: Set s -> Set (Pass s)
instance Passer '[] where
pass Empty = Empty
instance Passer '[e] where
pass (Ext e Empty) = Ext e Empty
instance (Passer ((Max e f) ': s), OrdH e f) => Passer (e ': f ': s) where
pass (Ext e (Ext f s)) = Ext (minH e f) (pass (Ext (maxH e f) s))
type family Min a b
type family Max a b
class OrdH e f where
minH :: e -> f -> Min e f
maxH :: e -> f -> Max e f
instance Show (Set '[]) where
show Empty = "{}"
instance (Show e, Show' (Set s)) => Show (Set (e ': s)) where
show (Ext e s) = "{" ++ show e ++ (show' s) ++ "}"
class Show' t where
show' :: t -> String
instance Show' (Set '[]) where
show' Empty = ""
instance (Show' (Set s), Show e) => Show' (Set (e ': s)) where
show' (Ext e s) = ", " ++ show e ++ (show' s)
class Split s t st where
split :: Set st -> (Set s, Set t)
instance Split '[] '[] '[] where
split Empty = (Empty, Empty)
instance Split s t st => Split (x ': s) (x ': t) (x ': st) where
split (Ext x st) = let (s, t) = split st
in (Ext x s, Ext x t)
instance Split s t st => Split (x ': s) t (x ': st) where
split (Ext x st) = let (s, t) = split st
in (Ext x s, t)
instance Split s t st => Split s (x ': t) (x ': st) where
split (Ext x st) = let (s, t) = split st
in (s, Ext x t)
class Subset s t where
subset :: Set t -> Set s
instance Subset '[] t where
subset xs = Empty
instance Subset s t => Subset (x ': s) (x ': t) where
subset (Ext x xs) = Ext x (subset xs)
instance Subset s t => Subset s (x ': t) where
subset (Ext _ xs) = subset xs