type-level-sets-0.8.9.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 # Instance detailsDefined in Data.Type.Set 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 # Instance detailsDefined in Data.Type.Set MethodsshowsPrec :: Int -> Set (e ': s) -> ShowS #show :: Set (e ': s) -> String #showList :: [Set (e ': s)] -> ShowS # Show (Set ([] :: [k])) Source # Instance detailsDefined in Data.Type.Set 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 Source #

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

Minimal complete definition

quicksort

Instances
 Sortable ([] :: [k]) Source # Instance detailsDefined in Data.Type.Set 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 :: [Type]) Source # Instance detailsDefined in Data.Type.Set 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

Methods

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

Instances
 Split s t st => Split (s :: [k2]) (x ': t :: [k1]) (x ': st :: [k1]) Source # Instance detailsDefined in Data.Type.Set Methodssplit :: Set (x ': st) -> (Set s, Set (x ': t)) Source # Split ([] :: [k1]) ([] :: [k2]) ([] :: [k3]) Source # Instance detailsDefined in Data.Type.Set Methodssplit :: Set [] -> (Set [], Set []) Source # Split s t st => Split (x ': s :: [k2]) (t :: [k1]) (x ': st :: [k2]) Source # Instance detailsDefined in Data.Type.Set Methodssplit :: Set (x ': st) -> (Set (x ': s), Set t) Source # Split s t st => Split (x ': s :: [k]) (x ': t :: [k]) (x ': st :: [k]) Source # Instance detailsDefined in Data.Type.Set 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 (k :: Symbol) (k' :: Symbol) Source # Instance detailsDefined in Data.Type.Map type Cmp (k :: Symbol) (k' :: Symbol) = CmpSymbol k k' type Cmp (k :-> v2 :: Mapping Symbol v1) (k' :-> v' :: Mapping Symbol v1) Source # Instance detailsDefined in Data.Type.Map type Cmp (k :-> v2 :: Mapping Symbol v1) (k' :-> v' :: Mapping Symbol 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

Methods

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

Instances
 Nubable ([] :: [k]) Source # Instance detailsDefined in Data.Type.Set Methodsnub :: Set [] -> Set (Nub []) Source # (Nub (e ': (f ': s)) ~ (e ': Nub (f ': s)), Nubable (f ': s)) => Nubable (e ': (f ': s) :: [k]) Source # Instance detailsDefined in Data.Type.Set Methodsnub :: Set (e ': (f ': s)) -> Set (Nub (e ': (f ': s))) Source # Nubable (e ': s) => Nubable (e ': (e ': s) :: [k]) Source # Instance detailsDefined in Data.Type.Set Methodsnub :: Set (e ': (e ': s)) -> Set (Nub (e ': (e ': s))) Source # Nubable (e ': ([] :: [k]) :: [k]) Source # Instance detailsDefined in Data.Type.Set 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

Methods

subset :: Set t -> Set s Source #

Instances
 Subset s t => Subset (s :: [k2]) (x ': t :: [k1]) Source # Instance detailsDefined in Data.Type.Set Methodssubset :: Set (x ': t) -> Set s Source # Subset ([] :: [k1]) ([] :: [k2]) Source # Instance detailsDefined in Data.Type.Set Methodssubset :: Set [] -> Set [] Source # Subset s t => Subset (x ': s :: [k]) (x ': t :: [k]) Source # Instance detailsDefined in Data.Type.Set 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 :: k) Source #

Constructors

 Proxy

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

class Remove s t Source #

Minimal complete definition

remove

Instances
 Remove ([] :: [k]) (t :: k) Source # Instance detailsDefined in Data.Type.Set Methodsremove :: Set [] -> Proxy t -> Set ([] :\ t) Source # (((y ': xs) :\ x) ~ (y ': (xs :\ x)), Remove xs x) => Remove (y ': xs :: [k]) (x :: k) Source # Instance detailsDefined in Data.Type.Set Methodsremove :: Set (y ': xs) -> Proxy x -> Set ((y ': xs) :\ x) Source # Remove xs x => Remove (x ': xs :: [k]) (x :: k) Source # Instance detailsDefined in Data.Type.Set Methodsremove :: Set (x ': xs) -> Proxy x -> Set ((x ': xs) :\ x) Source #

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

Delete elements from a set

Equations

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

class Member a s where Source #

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

Methods

member :: Proxy a -> Set s -> Bool Source #

Instances
 Member a s => Member (a :: k2) (b ': s :: [k1]) Source # Instance detailsDefined in Data.Type.Set Methodsmember :: Proxy a -> Set (b ': s) -> Bool Source # Member (a :: k) (a ': s :: [k]) Source # Instance detailsDefined in Data.Type.Set Methodsmember :: Proxy a -> Set (a ': s) -> Bool Source #

type NonMember a s = MemberP a s ~ False Source #

type family MemberP a s :: Bool where ... Source #

Equations

 MemberP a '[] = False MemberP a (a ': s) = True MemberP a (b ': s) = MemberP a s