type-level-sets-0.5: Type-level sets (with value-level counterparts and various operations)

Data.Type.Set

Synopsis

# Documentation

data Set n where Source #

Core Set definition, in terms of lists

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 (Append s t)) Source #

Union of sets

type Unionable s t = (Sortable (Append s t), Nubable (Sort (Append 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 (Append 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 Append (s :: [k]) (t :: [k]) :: [k] where ... Source #

List append (essentially set disjoint union)

Equations

 Append '[] t = t Append (x ': xs) ys = x ': Append 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 * ((:->) v a) ((:->) u b) Source # type Cmp * ((:->) v a) ((:->) u b) = CmpSymbol v u

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 #

data k :-> v infixl 2 Source #

Pair a symbol (represetning a variable) with a type

Constructors

 (Var k) :-> v infixl 2

Instances

 (Show (Var k), Show v) => Show ((:->) k v) Source # MethodsshowsPrec :: Int -> (k :-> v) -> ShowS #show :: (k :-> v) -> String #showList :: [k :-> v] -> ShowS # type Cmp * ((:->) v a) ((:->) u b) Source # type Cmp * ((:->) v a) ((:->) u b) = CmpSymbol v u

data Var k where Source #

Constructors

 Var :: Var k X :: Var "x" Some special defaults for some common names Y :: Var "y" Z :: Var "z"

Instances

 Show (Var v) Source # MethodsshowsPrec :: Int -> Var v -> ShowS #show :: Var v -> String #showList :: [Var v] -> ShowS # Show (Var "x") Source # MethodsshowsPrec :: Int -> Var "x" -> ShowS #show :: Var "x" -> String #showList :: [Var "x"] -> ShowS # Show (Var "y") Source # MethodsshowsPrec :: Int -> Var "y" -> ShowS #show :: Var "y" -> String #showList :: [Var "y"] -> ShowS # Show (Var "z") Source # MethodsshowsPrec :: Int -> Var "z" -> ShowS #show :: Var "z" -> String #showList :: [Var "z"] -> ShowS #