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

Data.Type.Set

Synopsis

Documentation

data Set (n :: [k]) :: * 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 # MethodsshowsPrec :: Int -> Set * ((* ': e) s) -> ShowS #show :: Set * ((* ': e) s) -> String #showList :: [Set * ((* ': e) s)] -> ShowS # Show (Set k ([] k)) Source # MethodsshowsPrec :: Int -> Set k [k] -> ShowS #show :: Set k [k] -> String #showList :: [Set k [k]] -> 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 k ([] k) Source # Methodsquicksort :: Set [k] xs -> Set [k] (Sort [k] xs) 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) xs -> Set ((* ': p) xs) (Sort ((* ': p) xs) 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 k2 k1 k1 s t st => Split k2 k1 k1 s ((:) k1 x t) ((:) k1 x st) Source # Methodssplit :: Set ((k1 ': x) st) st -> (Set s s, Set ((k1 ': x) t) t) Source # Split k1 k2 k3 ([] k1) ([] k2) ([] k3) Source # Methodssplit :: Set [k3] st -> (Set [k1] s, Set [k2] t) Source # Split k2 k1 k2 s t st => Split k2 k1 k2 ((:) k2 x s) t ((:) k2 x st) Source # Methodssplit :: Set ((k2 ': x) st) st -> (Set ((k2 ': x) s) s, Set t t) Source # Split k k k s t st => Split k k k ((:) k x s) ((:) k x t) ((:) k x st) Source # Methodssplit :: Set ((k ': x) st) st -> (Set ((k ': x) s) s, Set ((k ': x) t) 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 v1) ((:->) Symbol v1 k v2) ((:->) Symbol v1 k' v') Source # 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 ... 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 k ([] k) Source # Methodsnub :: Set [k] t -> Set [k] (Nub [k] t) Source # ((~) [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)) Source # Methodsnub :: Set ((k ': e) ((k ': f) s)) t -> Set ((k ': e) ((k ': f) s)) (Nub ((k ': e) ((k ': f) s)) t) Source # Nubable k ((:) k e s) => Nubable k ((:) k e ((:) k e s)) Source # Methodsnub :: Set ((k ': e) ((k ': e) s)) t -> Set ((k ': e) ((k ': e) s)) (Nub ((k ': e) ((k ': e) s)) t) Source # Nubable k ((:) k e ([] k)) Source # Methodsnub :: Set ((k ': e) [k]) t -> Set ((k ': e) [k]) (Nub ((k ': e) [k]) t) 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 k2 k1 s t => Subset k2 k1 s ((:) k1 x t) Source # Methodssubset :: Set ((k1 ': x) t) t -> Set s s Source # Subset k1 k2 ([] k1) ([] k2) Source # Methodssubset :: Set [k2] t -> Set [k1] s Source # Subset k k s t => Subset k k ((:) k x s) ((:) k x t) Source # Methodssubset :: Set ((k ': x) t) t -> Set ((k ': x) s) s Source #

type family Delete elem set where ... Source #

Equations

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

data Proxy (p :: k) Source #

Constructors

 Proxy

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

class Remove s t where Source #

Minimal complete definition

remove

Methods

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

Instances

 Remove k ([] k) t Source # Methodsremove :: Set [k] t -> Proxy [k] t -> Set [k] (([k] :\ t) t) Source # ((~) [k] ((:\) k ((:) k y xs) x) ((:) k y ((:\) k xs x)), Remove k xs x) => Remove k ((:) k y xs) x Source # Methodsremove :: Set ((k ': y) xs) x -> Proxy ((k ': y) xs) t -> Set ((k ': y) xs) (((k ': y) xs :\ x) t) Source # Remove k ((:) k x xs) x Source # Methodsremove :: Set ((k ': x) xs) x -> Proxy ((k ': x) xs) t -> Set ((k ': x) xs) (((k ': x) xs :\ x) t) Source #

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

Delete elements from a set

Equations

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

class Member a s Source #

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) Source # Methodsmember :: Proxy a a -> Set ((k1 ': b) s) s -> Bool Member k k a ((:) k a s) Source # Methodsmember :: Proxy a a -> Set ((k ': a) s) s -> Bool