effect-sessions-1.0: Sessions and session types for Concurrent Haskell

Safe Haskell None Haskell98

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 Show (Set ([] *)) Source

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

append :: Set s -> Set t -> Set (Append 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 Append s t :: [k] 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

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 * ((:->) v a) ((:->) u b) = CmpSymbol v u Source Symbol comparison type Cmp (Map Name Session) ((:->) Name Session c a) ((:->) Name Session d b) = CmpSessionMap ((:->) Name Session c a) ((:->) Name Session d b) Source Compare channel names for normalising type-level finite map representations

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 ([] *) ([] *) Source Subset ([] *) ((:) * x t) Source Subset s t => Subset ((:) * x s) ((:) * x t) Source

data k :-> v infixl 2 Source

Pair a symbol (representing a variable) with a type

Constructors

 (Var k) :-> v infixl 2

Instances

 (Show (Var k), Show v) => Show ((:->) k v) Source type Cmp * ((:->) v a) ((:->) u b) = CmpSymbol v u Source Symbol comparison

data Var k where Source

Constructors

 Var :: Var k X :: Var "x" Y :: Var "y" Z :: Var "z"

Instances

 Show (Var v) Source Show (Var "x") Source Show (Var "y") Source Show (Var "z") Source