type-level-sets-0.8.9.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
Updatable v t s ((v :-> t) ': s) Source # 
Instance details

Defined in Data.Type.Map

Methods

update :: Map s -> Var v -> t -> Map ((v :-> t) ': s) Source #

IsMember v t m => IsMember v t (x ': m) Source # 
Instance details

Defined in Data.Type.Map

Methods

lookp :: Var v -> Map (x ': m) -> t Source #

IsMember v t ((v :-> t) ': m) Source # 
Instance details

Defined in Data.Type.Map

Methods

lookp :: Var v -> Map ((v :-> t) ': m) -> t Source #

Updatable v t m n => Updatable v t ((w :-> y) ': m) ((w :-> y) ': n) Source # 
Instance details

Defined in Data.Type.Map

Methods

update :: Map ((w :-> y) ': m) -> Var v -> t -> Map ((w :-> y) ': n) Source #

Updatable v t ((v :-> s) ': m) ((v :-> t) ': m) Source # 
Instance details

Defined in Data.Type.Map

Methods

update :: Map ((v :-> s) ': m) -> Var v -> t -> Map ((v :-> t) ': m) Source #

Submap s t => Submap s (x ': t) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Split s t st => Split s (x ': t) (x ': st) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

(Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

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

Eq (Map ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

(==) :: Map [] -> Map [] -> Bool #

(/=) :: Map [] -> Map [] -> Bool #

(Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

compare :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Ordering #

(<) :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Bool #

(<=) :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Bool #

(>) :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Bool #

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

max :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) #

min :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) #

Ord (Map ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

compare :: Map [] -> Map [] -> Ordering #

(<) :: Map [] -> Map [] -> Bool #

(<=) :: Map [] -> Map [] -> Bool #

(>) :: Map [] -> Map [] -> Bool #

(>=) :: Map [] -> Map [] -> Bool #

max :: Map [] -> Map [] -> Map [] #

min :: Map [] -> Map [] -> Map [] #

(KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

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

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

Show (Map ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

showsPrec :: Int -> Map [] -> ShowS #

show :: Map [] -> String #

showList :: [Map []] -> ShowS #

Nubable ([] :: [Mapping Symbol Type]) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Submap ([] :: [Mapping Symbol Type]) ([] :: [Mapping Symbol Type]) Source # 
Instance details

Defined in Data.Type.Map

Methods

submap :: Map [] -> Map [] Source #

Split ([] :: [Mapping Symbol Type]) ([] :: [Mapping Symbol Type]) ([] :: [Mapping Symbol Type]) Source # 
Instance details

Defined in Data.Type.Map

Methods

split :: Map [] -> (Map [], Map []) Source #

(Nub (e ': (f ': s)) ~ (e ': Nub (f ': s)), Nubable (f ': s)) => Nubable (e ': (f ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Nubable (e ': ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

(Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': ((k :-> v') ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

nub :: Map ((k :-> v) ': ((k :-> v') ': s)) -> Map (Nub ((k :-> v) ': ((k :-> v') ': s))) Source #

Split s t st => Split (x ': s) t (x ': st) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Submap s t => Submap (x ': s) (x ': t) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Split s t st => Split (x ': s) (x ': t) (x ': st) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

type Cmp (k :-> v2 :: Mapping Symbol v1) (k' :-> v' :: Mapping Symbol v1) Source # 
Instance details

Defined in Data.Type.Map

type Cmp (k :-> v2 :: Mapping Symbol v1) (k' :-> v' :: Mapping Symbol v1) = 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 (normalising)

data Var (k :: Symbol) Source #

Pair a symbol (representing a variable) with a type

Constructors

Var 
Instances
KnownSymbol k => Show (Var k) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

show :: Var k -> String #

showList :: [Var k] -> ShowS #

data Map (n :: [Mapping Symbol *]) 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
(Eq v, Eq (Map s)) => Eq (Map ((k :-> v) ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

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

Eq (Map ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

(==) :: Map [] -> Map [] -> Bool #

(/=) :: Map [] -> Map [] -> Bool #

(Ord v, Ord (Map s)) => Ord (Map ((k :-> v) ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

compare :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Ordering #

(<) :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Bool #

(<=) :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Bool #

(>) :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Bool #

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

max :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) #

min :: Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) -> Map ((k :-> v) ': s) #

Ord (Map ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

compare :: Map [] -> Map [] -> Ordering #

(<) :: Map [] -> Map [] -> Bool #

(<=) :: Map [] -> Map [] -> Bool #

(>) :: Map [] -> Map [] -> Bool #

(>=) :: Map [] -> Map [] -> Bool #

max :: Map [] -> Map [] -> Map [] #

min :: Map [] -> Map [] -> Map [] #

(KnownSymbol k, Show v, Show' (Map s)) => Show (Map ((k :-> v) ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

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

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

Show (Map ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

showsPrec :: Int -> Map [] -> ShowS #

show :: Map [] -> String #

showList :: [Map []] -> ShowS #

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 #

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 (k :: Symbol) (k' :: Symbol) Source # 
Instance details

Defined in Data.Type.Map

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

Defined in Data.Type.Map

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

class Nubable t Source #

Minimal complete definition

nub

Instances
Nubable ([] :: [Mapping Symbol Type]) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

(Nub (e ': (f ': s)) ~ (e ': Nub (f ': s)), Nubable (f ': s)) => Nubable (e ': (f ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Nubable (e ': ([] :: [Mapping Symbol Type])) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

(Combinable v v', Nubable ((k :-> Combine v v') ': s)) => Nubable ((k :-> v) ': ((k :-> v') ': s)) Source # 
Instance details

Defined in Data.Type.Map

Methods

nub :: Map ((k :-> v) ': ((k :-> v') ': s)) -> Map (Nub ((k :-> v) ': ((k :-> v') ': s))) Source #

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

type family Lookup (m :: [Mapping k v]) (c :: k) :: Maybe v where ... Source #

Type-level lookup of 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 as type function

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 Source #

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

Minimal complete definition

split

Instances
Split s t st => Split s (x ': t) (x ': st) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Split ([] :: [Mapping Symbol Type]) ([] :: [Mapping Symbol Type]) ([] :: [Mapping Symbol Type]) Source # 
Instance details

Defined in Data.Type.Map

Methods

split :: Map [] -> (Map [], Map []) Source #

Split s t st => Split (x ': s) t (x ': st) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Split s t st => Split (x ': s) (x ': t) (x ': st) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

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

class IsMember v t m Source #

Membership test a type class (predicate)

Minimal complete definition

lookp

Instances
IsMember v t m => IsMember v t (x ': m) Source # 
Instance details

Defined in Data.Type.Map

Methods

lookp :: Var v -> Map (x ': m) -> t Source #

IsMember v t ((v :-> t) ': m) Source # 
Instance details

Defined in Data.Type.Map

Methods

lookp :: Var v -> Map ((v :-> t) ': m) -> t Source #

lookp :: IsMember v t m => Var v -> Map m -> t Source #

Value-level lookup of elements from a map, via type class predicate

class Updatable v t m n Source #

Updatability as a type class

Minimal complete definition

update

Instances
Updatable v t s ((v :-> t) ': s) Source # 
Instance details

Defined in Data.Type.Map

Methods

update :: Map s -> Var v -> t -> Map ((v :-> t) ': s) Source #

Updatable v t m n => Updatable v t ((w :-> y) ': m) ((w :-> y) ': n) Source # 
Instance details

Defined in Data.Type.Map

Methods

update :: Map ((w :-> y) ': m) -> Var v -> t -> Map ((w :-> y) ': n) Source #

Updatable v t ((v :-> s) ': m) ((v :-> t) ': m) Source # 
Instance details

Defined in Data.Type.Map

Methods

update :: Map ((v :-> s) ': m) -> Var v -> t -> Map ((v :-> t) ': m) Source #

update :: Updatable v t m n => Map m -> Var v -> t -> Map n Source #

Update a map with m at variable v with a value of type t to produce a map of type n

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 Source #

Construct a submap s from a supermap t

Minimal complete definition

submap

Instances
Submap s t => Submap s (x ': t) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

Submap ([] :: [Mapping Symbol Type]) ([] :: [Mapping Symbol Type]) Source # 
Instance details

Defined in Data.Type.Map

Methods

submap :: Map [] -> Map [] Source #

Submap s t => Submap (x ': s) (x ': t) Source # 
Instance details

Defined in Data.Type.Map

Methods

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

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