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

Safe HaskellSafe
LanguageHaskell98

Data.Type.Set

Synopsis

Documentation

data Set n where Source #

Constructors

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

Instances

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

Methods

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

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

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

Methods

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

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

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

Show (Set ([] *)) Source # 

Methods

showsPrec :: 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 # 

Methods

quicksort :: 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 # 

Methods

quicksort :: 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 # 

Methods

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

Split ([] *) ([] *) ([] *) Source # 

Methods

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

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

Methods

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

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

Methods

split :: 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' v') Source # 
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 ... 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 # 

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

Methods

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

Subset ([] *) ([] *) Source # 

Methods

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

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

Methods

subset :: 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