Data.Type.Map

Documentation

data Mapping k v

A key-value pair

Constructors

k :-> v infixr 4

Instances

Updatable v t ([] (Mapping Symbol *)) ((:) (Mapping Symbol *) ((:->) Symbol * v t) ([] (Mapping Symbol *)))

Methods

update :: Map [Mapping Symbol *] -> Var v -> t -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) [Mapping Symbol *])

IsMember v t m => IsMember v t ((:) (Mapping Symbol *) x m)

Methods

lookp :: Var v -> Map ((Mapping Symbol * ': x) m) -> t

IsMember v t ((:) (Mapping Symbol *) ((:->) Symbol * v t) m)

Methods

lookp :: Var v -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) m) -> t

Updatable v t m n => Updatable v t ((:) (Mapping Symbol *) ((:->) Symbol * w y) m) ((:) (Mapping Symbol *) ((:->) Symbol * w y) n)

Methods

update :: Map ((Mapping Symbol * ': (Symbol :-> *) w y) m) -> Var v -> t -> Map ((Mapping Symbol * ': (Symbol :-> *) w y) n)

Updatable v t ((:) (Mapping Symbol *) ((:->) Symbol * v s) m) ((:) (Mapping Symbol *) ((:->) Symbol * v t) m)

Methods

update :: Map ((Mapping Symbol * ': (Symbol :-> *) v s) m) -> Var v -> t -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) m)

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

Methods

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

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

Methods

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

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

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 *)))

Methods

(==) :: Map [Mapping Symbol *] -> Map [Mapping Symbol *] -> Bool

(/=) :: Map [Mapping Symbol *] -> Map [Mapping Symbol *] -> Bool

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

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 *)))

Methods

showsPrec :: Int -> Map [Mapping Symbol *] -> ShowS

show :: Map [Mapping Symbol *] -> String

showList :: [Map [Mapping Symbol *]] -> ShowS

Nubable ([] (Mapping Symbol *))

Methods

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

Submap ([] (Mapping Symbol *)) ([] (Mapping Symbol *))

Methods

submap :: Map [Mapping Symbol *] -> Map [Mapping Symbol *]

Split ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) ([] (Mapping Symbol *))

Methods

split :: Map [Mapping Symbol *] -> (Map [Mapping Symbol *], Map [Mapping Symbol *])

(Combinable v v', Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k (Combine * v v')) s)) => Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k v) ((:) (Mapping Symbol *) ((:->) Symbol * k v') s))

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)))

((~) [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))

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

Methods

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

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

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

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

Union of two finite maps

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

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

Union of two finite maps (normalising)

data Var (k :: Symbol)

Pair a symbol (representing a variable) with a type

Constructors

Var

Instances

KnownSymbol k => Show (Var k)

Methods

showsPrec :: Int -> Var k -> ShowS

show :: Var k -> String

showList :: [Var k] -> ShowS

data Map (n :: [Mapping Symbol *]) where

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))

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 *)))

Methods

(==) :: Map [Mapping Symbol *] -> Map [Mapping Symbol *] -> Bool

(/=) :: Map [Mapping Symbol *] -> Map [Mapping Symbol *] -> Bool

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

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 *)))

Methods

showsPrec :: Int -> Map [Mapping Symbol *] -> ShowS

show :: Map [Mapping Symbol *] -> String

showList :: [Map [Mapping Symbol *]] -> ShowS

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

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

class Combinable t t' where

Minimal complete definition

combine

Methods

combine :: t -> t' -> Combine t t'

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

Open-family for the ordering operation in the sort

Instances

type Cmp Symbol k k'

type Cmp Symbol k k' = CmpSymbol k k'

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

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

class Nubable t where

Minimal complete definition

nub

Methods

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

Instances

Nubable ([] (Mapping Symbol *))

Methods

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

(Combinable v v', Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k (Combine * v v')) s)) => Nubable ((:) (Mapping Symbol *) ((:->) Symbol * k v) ((:) (Mapping Symbol *) ((:->) Symbol * k v') s))

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)))

((~) [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))

Methods

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

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

Methods

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

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

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

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 ...

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 ...

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

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)

Instances

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

Methods

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

Split ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) ([] (Mapping Symbol *))

Methods

split :: Map [Mapping Symbol *] -> (Map [Mapping Symbol *], Map [Mapping Symbol *])

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

Methods

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

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

Methods

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

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

class IsMember v t m where

Membership test a type class (predicate)

Minimal complete definition

lookp

Methods

lookp :: Var v -> Map m -> t

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

Instances

IsMember v t m => IsMember v t ((:) (Mapping Symbol *) x m)

Methods

lookp :: Var v -> Map ((Mapping Symbol * ': x) m) -> t

IsMember v t ((:) (Mapping Symbol *) ((:->) Symbol * v t) m)

Methods

lookp :: Var v -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) m) -> t

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

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

class Updatable v t m n where

Updatability as a type class

Minimal complete definition

update

Methods

update :: Map m -> Var v -> t -> Map n

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

Instances

Updatable v t ([] (Mapping Symbol *)) ((:) (Mapping Symbol *) ((:->) Symbol * v t) ([] (Mapping Symbol *)))

Methods

update :: Map [Mapping Symbol *] -> Var v -> t -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) [Mapping Symbol *])

Updatable v t m n => Updatable v t ((:) (Mapping Symbol *) ((:->) Symbol * w y) m) ((:) (Mapping Symbol *) ((:->) Symbol * w y) n)

Methods

update :: Map ((Mapping Symbol * ': (Symbol :-> *) w y) m) -> Var v -> t -> Map ((Mapping Symbol * ': (Symbol :-> *) w y) n)

Updatable v t ((:) (Mapping Symbol *) ((:->) Symbol * v s) m) ((:) (Mapping Symbol *) ((:->) Symbol * v t) m)

Methods

update :: Map ((Mapping Symbol * ': (Symbol :-> *) v s) m) -> Var v -> t -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) m)

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

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)

Predicate to check if in normalised map form

type AsMap s = Nub (Sort s)

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

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

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

class Submap s t where

Construct a submap s from a supermap t

Minimal complete definition

submap

Methods

submap :: Map t -> Map s

Instances

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

Methods

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

Submap ([] (Mapping Symbol *)) ([] (Mapping Symbol *))

Methods

submap :: Map [Mapping Symbol *] -> Map [Mapping Symbol *]

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

Methods

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

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