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

Safe HaskellNone
LanguageHaskell98

Data.Type.Set

Synopsis

Documentation

data Set n where Source

Constructors

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

Instances

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

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

append :: Set s -> Set t -> Set (s :++ t) Source

type family Sort xs :: [k] 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

Methods

quicksort :: Set xs -> Set (Sort xs) Source

Instances

Sortable ([] *) Source 
(Sortable (Filter * FMin p xs), Sortable (Filter * FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable ((:) * p xs) Source 

type family x :++ y :: [k] 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 ((:) * x t) ((:) * x st) Source 
Split ([] *) ([] *) ([] *) Source 
Split s t st => Split ((:) * x s) t ((:) * x st) Source 
Split s t st => Split ((:) * x s) ((:) * x t) ((:) * x st) Source 

type family Cmp a b :: Ordering Source

Open-family for the ordering operation in the sort

Instances

type Cmp Symbol k k' = CmpSymbol k k' Source 
type Cmp (Mapping Symbol k) ((:->) Symbol k k1 v) ((:->) Symbol k k' v') = CmpSymbol k1 k' Source 

type family Filter f p xs :: [k] 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 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 ([] *) Source 
((~) [*] (Nub * ((:) * e ((:) * f s))) ((:) * e (Nub * ((:) * f s))), Nubable ((:) * f s)) => Nubable ((:) * e ((:) * f s)) Source 
Nubable ((:) * e s) => Nubable ((:) * e ((:) * e s)) Source 
Nubable ((:) * 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 ((:) * x t) Source 
Subset ([] *) ([] *) Source 
Subset s t => Subset ((:) * x s) ((:) * x t) Source 

type family Delete elem set Source

Equations

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

data Proxy p Source

Constructors

Proxy