Data.Type.Set

Documentation

data Set (n :: [k]) where

Constructors

Empty :: Set '[]

Ext :: e -> Set s -> Set (e ': s)

Instances

(Eq e, Eq (Set s)) => Eq (Set (e ': s))

Defined 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))

Defined in Data.Type.Set

Methods

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

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

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

Show (Set ([] :: [k]))

Defined in Data.Type.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

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

Minimal complete definition

quicksort

Instances

Sortable ([] :: [k])

Defined in Data.Type.Set

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 :: [Type])

Defined in Data.Type.Set

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

Methods

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

Instances

Split s t st => Split (s :: [k2]) (x ': t :: [k1]) (x ': st :: [k1])

Defined in Data.Type.Set

Methods

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

Split ([] :: [k1]) ([] :: [k2]) ([] :: [k3])

Defined in Data.Type.Set

Methods

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

Split s t st => Split (x ': s :: [k2]) (t :: [k1]) (x ': st :: [k2])

Defined in Data.Type.Set

Methods

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

Split s t st => Split (x ': s :: [k]) (x ': t :: [k]) (x ': st :: [k])

Defined in Data.Type.Set

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 (k :: Symbol) (k' :: Symbol)

Defined 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)

Defined 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 ...

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

Methods

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

Instances

Nubable ([] :: [k])

Defined in Data.Type.Set

Methods

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

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

Defined in Data.Type.Set

Methods

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

Nubable (e ': s) => Nubable (e ': (e ': s) :: [k])

Defined in Data.Type.Set

Methods

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

Nubable (e ': ([] :: [k]) :: [k])

Defined in Data.Type.Set

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

Methods

subset :: Set t -> Set s

Instances

Subset s t => Subset (s :: [k2]) (x ': t :: [k1])

Defined in Data.Type.Set

Methods

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

Subset ([] :: [k1]) ([] :: [k2])

Defined in Data.Type.Set

Methods

subset :: Set [] -> Set []

Subset s t => Subset (x ': s :: [k]) (x ': t :: [k])

Defined in Data.Type.Set

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 :: k)

Constructors

Proxy

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

class Remove s t

Minimal complete definition

remove

Instances

Remove ([] :: [k]) (t :: k)

Defined in Data.Type.Set

Methods

remove :: Set [] -> Proxy t -> Set ([] :\ t)

(((y ': xs) :\ x) ~ (y ': (xs :\ x)), Remove xs x) => Remove (y ': xs :: [k]) (x :: k)

Defined in Data.Type.Set

Methods

remove :: Set (y ': xs) -> Proxy x -> Set ((y ': xs) :\ x)

Remove xs x => Remove (x ': xs :: [k]) (x :: k)

Defined in Data.Type.Set

Methods

remove :: Set (x ': xs) -> Proxy x -> Set ((x ': xs) :\ x)

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

Delete elements from a set

Equations

'[] :\ x = '[]

(x ': xs) :\ x = xs :\ x

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

class Member a s where

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

Methods

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

Instances

Member a s => Member (a :: k2) (b ': s :: [k1])

Defined in Data.Type.Set

Methods

member :: Proxy a -> Set (b ': s) -> Bool

Member (a :: k) (a ': s :: [k])

Defined in Data.Type.Set

Methods

member :: Proxy a -> Set (a ': s) -> Bool

type NonMember a s = MemberP a s ~ False

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

Equations

MemberP a '[] = False

MemberP a (a ': s) = True

MemberP a (b ': s) = MemberP a s