type-level-sets-0.6.1: Type-level sets and finite maps (with value-level counterparts)

Data.Type.Set

Synopsis

# Documentation

data Set n where Source #

Constructors

 Empty :: Set '[] Ext :: e -> Set s -> Set (e ': s)

Instances

 (Show e, Show' (Set s)) => Show (Set ((:) * e s)) Source # MethodsshowsPrec :: Int -> Set ((* ': e) s) -> ShowS #show :: Set ((* ': e) s) -> String #showList :: [Set ((* ': e) s)] -> ShowS # Show (Set ([] *)) Source # MethodsshowsPrec :: Int -> Set [*] -> ShowS #show :: Set [*] -> String #showList :: [Set [*]] -> ShowS #

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

Union of sets

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

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

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

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

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

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 Source #

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

Minimal complete definition

quicksort

Methods

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

Instances

 Sortable ([] *) Source # Methodsquicksort :: Set [*] -> Set (Sort * [*]) Source # (Sortable (Filter * FMin p xs), Sortable (Filter * FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable ((:) * p xs) Source # Methodsquicksort :: Set ((* ': p) xs) -> Set (Sort * ((* ': p) xs)) Source #

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

List append (essentially set disjoint union)

Equations

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

class Split s t st where Source #

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) Source #

Instances

 Split s t st => Split s ((:) * x t) ((:) * x st) Source # Methodssplit :: Set ((* ': x) st) -> (Set s, Set ((* ': x) t)) Source # Split ([] *) ([] *) ([] *) Source # Methodssplit :: Set [*] -> (Set [*], Set [*]) Source # Split s t st => Split ((:) * x s) t ((:) * x st) Source # Methodssplit :: Set ((* ': x) st) -> (Set ((* ': x) s), Set t) Source # Split s t st => Split ((:) * x s) ((:) * x t) ((:) * x st) Source # Methodssplit :: Set ((* ': x) st) -> (Set ((* ': x) s), Set ((* ': x) t)) Source #

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

Open-family for the ordering operation in the sort

Instances

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

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

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 Source #

Constructors

 FMin FMax

type family Nub t where ... Source #

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 Source #

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) Source #

Instances

 Nubable ([] *) Source # Methodsnub :: Set [*] -> Set (Nub * [*]) Source # ((~) [*] (Nub * ((:) * e ((:) * f s))) ((:) * e (Nub * ((:) * f s))), Nubable ((:) * f s)) => Nubable ((:) * e ((:) * f s)) Source # Methodsnub :: Set ((* ': e) ((* ': f) s)) -> Set (Nub * ((* ': e) ((* ': f) s))) Source # Nubable ((:) * e s) => Nubable ((:) * e ((:) * e s)) Source # Methodsnub :: Set ((* ': e) ((* ': e) s)) -> Set (Nub * ((* ': e) ((* ': e) s))) Source # Nubable ((:) * e ([] *)) Source # Methodsnub :: Set ((* ': e) [*]) -> Set (Nub * ((* ': e) [*])) Source #

type AsSet s = Nub (Sort s) Source #

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

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

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

type IsSet s = s ~ Nub (Sort s) Source #

Predicate to check if in the set form

class Subset s t where Source #

Construct a subsetset s from a superset t

Minimal complete definition

subset

Methods

subset :: Set t -> Set s Source #

Instances

 Subset ([] *) ([] *) Source # Methodssubset :: Set [*] -> Set [*] Source # Subset ([] *) ((:) * x t) Source # Methodssubset :: Set ((* ': x) t) -> Set [*] Source # Subset s t => Subset ((:) * x s) ((:) * x t) Source # Methodssubset :: Set ((* ': x) t) -> Set ((* ': x) s) Source #

type family Delete elem set where ... Source #

Equations

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

data Proxy p Source #

Constructors

 Proxy