Data.Type.Set

Documentation

data Set n 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 ([] *))

Methods

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

show :: Set [*] -> String

showList :: [Set [*]] -> 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 ([] *)

Methods

quicksort :: Set [*] -> Set (Sort * [*])

(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) -> Set (Sort * ((* ': p) 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 s t st => Split s ((:) * x t) ((:) * x st)

Methods

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

Split ([] *) ([] *) ([] *)

Methods

split :: Set [*] -> (Set [*], Set [*])

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

Methods

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

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

Methods

split :: Set ((* ': x) st) -> (Set ((* ': x) s), Set ((* ': x) 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 v) ((:->) Symbol v k v1) ((:->) Symbol v k' v')

type Cmp (Mapping Symbol v) ((:->) Symbol v k v1) ((:->) Symbol v 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 ([] *)

Methods

nub :: Set [*] -> Set (Nub * [*])

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

Methods

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

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

Methods

nub :: Set ((* ': e) ((* ': e) s)) -> Set (Nub * ((* ': e) ((* ': e) s)))

Nubable ((:) * e ([] *))

Methods

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

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 s t => Subset s ((:) * x t)

Methods

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

Subset ([] *) ([] *)

Methods

subset :: Set [*] -> Set [*]

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

Methods

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

type family Delete elem set where ...

Equations

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

data Proxy p

Constructors

Proxy