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

Safe HaskellNone
LanguageHaskell98

Data.Type.Map

Synopsis

Documentation

data Mapping k v Source

A key-value pair

Constructors

k :-> v infixr 4 

Instances

Submap s t => Submap s ((:) (Mapping Symbol *) x t) Source 
Split s t st => Split s ((:) (Mapping Symbol *) x t) ((:) (Mapping Symbol *) x st) Source 
(KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((:) (Mapping Symbol *) ((:->) Symbol * k v) s)) Source 
Show (Map ([] (Mapping Symbol *))) Source 
Nubable ([] (Mapping Symbol *)) Source 
Submap ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) Source 
Split ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) Source 
((~) [Mapping Symbol *] (Nub Symbol * ((:) (Mapping Symbol *) e ((:) (Mapping Symbol *) f s))) ((:) (Mapping Symbol *) e (Nub Symbol * ((:) (Mapping Symbol *) f s))), Nubable ((:) (Mapping Symbol *) f s)) => Nubable ((:) (Mapping Symbol *) e ((:) (Mapping Symbol *) f s)) Source 
Nubable ((:) (Mapping Symbol *) e ([] (Mapping Symbol *))) Source 
(Combinable v v', Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k (Combine * v v')) s)) => Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k v) ((:) (Mapping Symbol *) ((:->) Symbol * k v') s)) Source 
Split s t st => Split ((:) (Mapping Symbol *) x s) t ((:) (Mapping Symbol *) x st) Source 
Submap s t => Submap ((:) (Mapping Symbol *) x s) ((:) (Mapping Symbol *) x t) Source 
Split s t st => Split ((:) (Mapping Symbol *) x s) ((:) (Mapping Symbol *) x t) ((:) (Mapping Symbol *) x st) Source 
type Cmp (Mapping Symbol k) ((:->) Symbol k k1 v) ((:->) Symbol k k' v') = CmpSymbol k1 k' Source 

type Union m n = Nub (Sort (m :++ n)) Source

Union of two finite maps

type Unionable s t = (Nubable (Sort (s :++ t)), Sortable (s :++ t)) Source

union :: Unionable s t => Map s -> Map t -> Map (Union s t) Source

Union of two finite maps

data Var k Source

Pair a symbol (representing a variable) with a type

Constructors

Var 

Instances

data Map n where Source

A value-level heterogenously-typed Map (with type-level representation in terms of lists)

Constructors

Empty :: Map `[]` 
Ext :: Var k -> v -> Map m -> Map ((k :-> v) : m) 

Instances

(KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((:) (Mapping Symbol *) ((:->) Symbol * k v) s)) Source 
Show (Map ([] (Mapping Symbol *))) Source 

type family Combine a b :: v Source

Open type family for combining values in a map (that have the same key)

class Combinable t t' where Source

Methods

combine :: t -> t' -> Combine t t' 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 

class Nubable t where Source

Methods

nub :: Map t -> Map (Nub t) Source

Instances

Nubable ([] (Mapping Symbol *)) Source 
((~) [Mapping Symbol *] (Nub Symbol * ((:) (Mapping Symbol *) e ((:) (Mapping Symbol *) f s))) ((:) (Mapping Symbol *) e (Nub Symbol * ((:) (Mapping Symbol *) f s))), Nubable ((:) (Mapping Symbol *) f s)) => Nubable ((:) (Mapping Symbol *) e ((:) (Mapping Symbol *) f s)) Source 
Nubable ((:) (Mapping Symbol *) e ([] (Mapping Symbol *))) Source 
(Combinable v v', Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k (Combine * v v')) s)) => Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k v) ((:) (Mapping Symbol *) ((:->) Symbol * k v') s)) Source 

type family Lookup m c :: Maybe v Source

Lookup elements from a map

Equations

Lookup `[]` k = Nothing 
Lookup ((k :-> v) : m) k = Just v 
Lookup (kvp : m) k = Lookup m k 

type family Member c m :: Bool Source

Membership test

Equations

Member k `[]` = False 
Member k ((k :-> v) : m) = True 
Member k (kvp : m) = Member k m 

type family m :\ c :: [Mapping k v] Source

Delete elements from a map by key

Equations

`[]` :\ k = `[]` 
((k :-> v) : m) :\ k = m :\ k 
(kvp : m) :\ k = kvp : (m :\ k) 

class Split s t st where Source

Splitting a union of maps, given the maps we want to split it into

Methods

split :: Map st -> (Map s, Map t) Source

Instances

Split s t st => Split s ((:) (Mapping Symbol *) x t) ((:) (Mapping Symbol *) x st) Source 
Split ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) Source 
Split s t st => Split ((:) (Mapping Symbol *) x s) t ((:) (Mapping Symbol *) x st) Source 
Split s t st => Split ((:) (Mapping Symbol *) x s) ((:) (Mapping Symbol *) x t) ((:) (Mapping Symbol *) x st) Source 

type IsMap s = s ~ Nub (Sort s) Source

Predicate to check if in normalised map form

type AsMap s = Nub (Sort s) Source

At the type level, normalise the list form to the map form

asMap :: (Sortable s, Nubable (Sort s)) => Map s -> Map (AsMap s) Source

At the value level, noramlise the list form to the map form

class Submap s t where Source

Construct a submap s from a supermap t

Methods

submap :: Map t -> Map s Source

Instances

Submap s t => Submap s ((:) (Mapping Symbol *) x t) Source 
Submap ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) Source 
Submap s t => Submap ((:) (Mapping Symbol *) x s) ((:) (Mapping Symbol *) x t) Source