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

Safe HaskellSafe
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 # 

Methods

submap :: Map ((Mapping Symbol * ': x) t) -> Map s Source #

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

Methods

split :: Map ((Mapping Symbol * ': x) st) -> (Map s, Map ((Mapping Symbol * ': x) t)) Source #

(KnownSymbol k, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((:) (Mapping Symbol *) ((:->) Symbol * k v) s)) Source # 

Methods

(==) :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Bool #

(/=) :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Bool #

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

Methods

showsPrec :: Int -> Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> ShowS #

show :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> String #

showList :: [Map ((Mapping Symbol * ': (Symbol :-> *) k v) s)] -> ShowS #

Show (Map ([] (Mapping Symbol *))) Source # 
Nubable ([] (Mapping Symbol *)) Source # 

Methods

nub :: Map [Mapping Symbol *] -> Map (Nub Symbol * [Mapping Symbol *]) Source #

Submap ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) Source # 
Split ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) ([] (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 # 

Methods

nub :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) ((Mapping Symbol * ': (Symbol :-> *) k v') s)) -> Map (Nub Symbol * ((Mapping Symbol * ': (Symbol :-> *) k v) ((Mapping Symbol * ': (Symbol :-> *) k v') s))) 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 # 

Methods

nub :: Map ((Mapping Symbol * ': e) ((Mapping Symbol * ': f) s)) -> Map (Nub Symbol * ((Mapping Symbol * ': e) ((Mapping Symbol * ': f) s))) Source #

Nubable ((:) (Mapping Symbol *) e ([] (Mapping Symbol *))) Source # 

Methods

nub :: Map ((Mapping Symbol * ': e) [Mapping Symbol *]) -> Map (Nub Symbol * ((Mapping Symbol * ': e) [Mapping Symbol *])) Source #

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

Methods

split :: Map ((Mapping Symbol * ': x) st) -> (Map ((Mapping Symbol * ': x) s), Map t) Source #

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

Methods

submap :: Map ((Mapping Symbol * ': x) t) -> Map ((Mapping Symbol * ': x) s) Source #

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

Methods

split :: Map ((Mapping Symbol * ': x) st) -> (Map ((Mapping Symbol * ': x) s), Map ((Mapping Symbol * ': x) t)) Source #

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

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

KnownSymbol k => Show (Var k) Source # 

Methods

showsPrec :: Int -> Var k -> ShowS #

show :: Var k -> String #

showList :: [Var k] -> ShowS #

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, Eq (Var k), Eq v, Eq (Map s)) => Eq (Map ((:) (Mapping Symbol *) ((:->) Symbol * k v) s)) Source # 

Methods

(==) :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Bool #

(/=) :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> Bool #

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

Methods

showsPrec :: Int -> Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> ShowS #

show :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> String #

showList :: [Map ((Mapping Symbol * ': (Symbol :-> *) k v) s)] -> ShowS #

Show (Map ([] (Mapping Symbol *))) Source # 

type family Combine (a :: v) (b :: v) :: v Source #

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

class Combinable t t' where Source #

Minimal complete definition

combine

Methods

combine :: t -> t' -> Combine t t' Source #

type family Cmp (a :: k) (b :: k) :: Ordering Source #

Open-family for the ordering operation in the sort

Instances

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

class Nubable t where Source #

Minimal complete definition

nub

Methods

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

Instances

Nubable ([] (Mapping Symbol *)) Source # 

Methods

nub :: Map [Mapping Symbol *] -> Map (Nub Symbol * [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 # 

Methods

nub :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) ((Mapping Symbol * ': (Symbol :-> *) k v') s)) -> Map (Nub Symbol * ((Mapping Symbol * ': (Symbol :-> *) k v) ((Mapping Symbol * ': (Symbol :-> *) k v') s))) 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 # 

Methods

nub :: Map ((Mapping Symbol * ': e) ((Mapping Symbol * ': f) s)) -> Map (Nub Symbol * ((Mapping Symbol * ': e) ((Mapping Symbol * ': f) s))) Source #

Nubable ((:) (Mapping Symbol *) e ([] (Mapping Symbol *))) Source # 

Methods

nub :: Map ((Mapping Symbol * ': e) [Mapping Symbol *]) -> Map (Nub Symbol * ((Mapping Symbol * ': e) [Mapping Symbol *])) Source #

nub :: Nubable t => Map t -> Map (Nub t) Source #

type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where ... 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 :: k) (m :: [Mapping k v]) :: Bool where ... Source #

Membership test

Equations

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

type family (m :: [Mapping k v]) :\ (c :: k) :: [Mapping k v] where ... 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

Minimal complete definition

split

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 # 

Methods

split :: Map ((Mapping Symbol * ': x) st) -> (Map s, Map ((Mapping Symbol * ': x) t)) Source #

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

Methods

split :: Map ((Mapping Symbol * ': x) st) -> (Map ((Mapping Symbol * ': x) s), Map t) Source #

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

Methods

split :: Map ((Mapping Symbol * ': x) st) -> (Map ((Mapping Symbol * ': x) s), Map ((Mapping Symbol * ': x) t)) Source #

split :: Split s t st => Map st -> (Map s, Map t) 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

Minimal complete definition

submap

Methods

submap :: Map t -> Map s Source #

Instances

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

Methods

submap :: Map ((Mapping Symbol * ': x) t) -> Map s Source #

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

Methods

submap :: Map ((Mapping Symbol * ': x) t) -> Map ((Mapping Symbol * ': x) s) Source #

submap :: Submap s t => Map t -> Map s Source #