Data.Type.Set

Documentation

data Set (n :: [k]) :: * where

Constructors

Empty :: Set '[]

Ext :: e -> Set s -> Set (e ': s)

Instances

(Eq e, Eq (Set * s)) => Eq (Set * ((:) * e s))

Methods

(==) :: Set * ((* ': e) s) -> Set * ((* ': e) s) -> Bool

(/=) :: Set * ((* ': e) s) -> Set * ((* ': e) s) -> Bool

(Show e, Show' (Set * s)) => Show (Set * ((:) * e s))

Methods

showsPrec :: Int -> Set * ((* ': e) s) -> ShowS

show :: Set * ((* ': e) s) -> String

showList :: [Set * ((* ': e) s)] -> ShowS

Show (Set k ([] k))

Methods

showsPrec :: Int -> Set k [k] -> ShowS

show :: Set k [k] -> String

showList :: [Set k [k]] -> ShowS

type Union s t = Nub (Sort (s :++ t))

Union of sets

type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)))

union :: Unionable s t => Set s -> Set t -> Set (Union s t)

quicksort :: Sortable xs => Set xs -> Set (Sort xs)

append :: Set s -> Set t -> Set (s :++ t)

type family Sort (xs :: [k]) :: [k] where ...

Type-level quick sort for normalising the representation of sets

Equations

Sort '[] = '[]

Sort (x ': xs) = (Sort (Filter FMin x xs) :++ '[x]) :++ Sort (Filter FMax x xs)

class Sortable xs where

Value-level quick sort that respects the type-level ordering

Minimal complete definition

quicksort

Methods

quicksort :: Set xs -> Set (Sort xs)

Instances

Sortable k ([] k)

Methods

quicksort :: Set [k] xs -> Set [k] (Sort [k] xs)

(Sortable * (Filter * FMin p xs), Sortable * (Filter * FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable * ((:) * p xs)

Methods

quicksort :: Set ((* ': p) xs) xs -> Set ((* ': p) xs) (Sort ((* ': p) xs) xs)

type family (x :: [k]) :++ (y :: [k]) :: [k] where ...

List append (essentially set disjoint union)

Equations

'[] :++ xs = xs

(x ': xs) :++ ys = x ': (xs :++ ys)

class Split s t st where

Splitting a union a set, given the sets we want to split it into

Minimal complete definition

split

Methods

split :: Set st -> (Set s, Set t)

Instances

Split k2 k1 k1 s t st => Split k2 k1 k1 s ((:) k1 x t) ((:) k1 x st)

Methods

split :: Set ((k1 ': x) st) st -> (Set s s, Set ((k1 ': x) t) t)

Split k1 k2 k3 ([] k1) ([] k2) ([] k3)

Methods

split :: Set [k3] st -> (Set [k1] s, Set [k2] t)

Split k2 k1 k2 s t st => Split k2 k1 k2 ((:) k2 x s) t ((:) k2 x st)

Methods

split :: Set ((k2 ': x) st) st -> (Set ((k2 ': x) s) s, Set t t)

Split k k k s t st => Split k k k ((:) k x s) ((:) k x t) ((:) k x st)

Methods

split :: Set ((k ': x) st) st -> (Set ((k ': x) s) s, Set ((k ': x) t) t)

type family Cmp (a :: k) (b :: k) :: Ordering

Open-family for the ordering operation in the sort

Instances

type Cmp Symbol k k'

type Cmp Symbol k k' = CmpSymbol k k'

type Cmp (Mapping Symbol v1) ((:->) Symbol v1 k v2) ((:->) Symbol v1 k' v')

type Cmp (Mapping Symbol v1) ((:->) Symbol v1 k v2) ((:->) Symbol v1 k' v') = CmpSymbol k k'

type family Filter (f :: Flag) (p :: k) (xs :: [k]) :: [k] where ...

Equations

Filter f p '[] = '[]

Filter FMin p (x ': xs) = If (Cmp x p == LT) (x ': Filter FMin p xs) (Filter FMin p xs)

Filter FMax p (x ': xs) = If ((Cmp x p == GT) || (Cmp x p == EQ)) (x ': Filter FMax p xs) (Filter FMax p xs)

data Flag

Constructors

FMin

FMax

type family Nub t where ...

Remove duplicates from a sorted list

Equations

Nub '[] = '[]

Nub '[e] = '[e]

Nub (e ': (e ': s)) = Nub (e ': s)

Nub (e ': (f ': s)) = e ': Nub (f ': s)

class Nubable t where

Value-level counterpart to the type-level Nub Note: the value-level case for equal types is not define here, but should be given per-application, e.g., custom merging behaviour may be required

Minimal complete definition

nub

Methods

nub :: Set t -> Set (Nub t)

Instances

Nubable k ([] k)

Methods

nub :: Set [k] t -> Set [k] (Nub [k] t)

((~) [k] (Nub k ((:) k e ((:) k f s))) ((:) k e (Nub k ((:) k f s))), Nubable k ((:) k f s)) => Nubable k ((:) k e ((:) k f s))

Methods

nub :: Set ((k ': e) ((k ': f) s)) t -> Set ((k ': e) ((k ': f) s)) (Nub ((k ': e) ((k ': f) s)) t)

Nubable k ((:) k e s) => Nubable k ((:) k e ((:) k e s))

Methods

nub :: Set ((k ': e) ((k ': e) s)) t -> Set ((k ': e) ((k ': e) s)) (Nub ((k ': e) ((k ': e) s)) t)

Nubable k ((:) k e ([] k))

Methods

nub :: Set ((k ': e) [k]) t -> Set ((k ': e) [k]) (Nub ((k ': e) [k]) t)

type AsSet s = Nub (Sort s)

At the type level, normalise the list form to the set form

asSet :: (Sortable s, Nubable (Sort s)) => Set s -> Set (AsSet s)

At the value level, noramlise the list form to the set form

type IsSet s = s ~ Nub (Sort s)

Predicate to check if in the set form

class Subset s t where

Construct a subsetset s from a superset t

Minimal complete definition

subset

Methods

subset :: Set t -> Set s

Instances

Subset k2 k1 s t => Subset k2 k1 s ((:) k1 x t)

Methods

subset :: Set ((k1 ': x) t) t -> Set s s

Subset k1 k2 ([] k1) ([] k2)

Methods

subset :: Set [k2] t -> Set [k1] s

Subset k k s t => Subset k k ((:) k x s) ((:) k x t)

Methods

subset :: Set ((k ': x) t) t -> Set ((k ': x) s) s

type family Delete elem set where ...

Equations

Delete elem (Set xs) = Set (DeleteFromList elem xs)

data Proxy (p :: k)

Constructors

Proxy

remove :: Remove s t => Set s -> Proxy t -> Set (s :\ t)

class Remove s t where

Minimal complete definition

remove

Methods

remove :: Set s -> Proxy t -> Set (s :\ t)

Instances

Remove k ([] k) t

Methods

remove :: Set [k] t -> Proxy [k] t -> Set [k] (([k] :\ t) t)

((~) [k] ((:\) k ((:) k y xs) x) ((:) k y ((:\) k xs x)), Remove k xs x) => Remove k ((:) k y xs) x

Methods

remove :: Set ((k ': y) xs) x -> Proxy ((k ': y) xs) t -> Set ((k ': y) xs) (((k ': y) xs :\ x) t)

Remove k ((:) k x xs) x

Methods

remove :: Set ((k ': x) xs) x -> Proxy ((k ': x) xs) t -> Set ((k ': x) xs) (((k ': x) xs :\ x) t)

type family (m :: [k]) :\ (x :: k) :: [k] where ...

Delete elements from a set

Equations

'[] :\ x = '[]

(x ': xs) :\ x = xs

(y ': xs) :\ x = y ': (xs :\ x)

class Member a s

Membership of an element in a set, with an acommanying value-level function that returns a bool

Minimal complete definition

member

Instances

Member k2 k1 a s => Member k2 k1 a ((:) k1 b s)

Methods

member :: Proxy a a -> Set ((k1 ': b) s) s -> Bool

Member k k a ((:) k a s)

Methods

member :: Proxy a a -> Set ((k ': a) s) s -> Bool