Safe Haskell	None
Language	Haskell98

Control.Effect.Writer

Contents

Orphan instances

Synopsis

Documentation

data Writer (w :: [Mapping Symbol *]) a Source #

Provides an effect-parameterised version of the writer monad. Effects are maps of variable-type pairs, providing an effect system for writer effects.

Constructors

Writer
Fields runWriter :: (a, Map w)

Instances

Effect [Mapping Symbol *] Writer Source #
Associated Types type Unit Writer (m :: Writer -> * -> ) :: k Source # type Plus Writer (m :: Writer -> -> ) (f :: Writer) (g :: Writer) :: k Source # type Inv Writer (m :: Writer -> -> *) (f :: Writer) (g :: Writer) :: Constraint Source # Methods return :: a -> m (Unit Writer m) a Source # (>>=) :: Inv Writer m f g => m f a -> (a -> m g b) -> m (Plus Writer m f g) b Source # (>>) :: Inv Writer m f g => m f a -> m g b -> m (Plus Writer m f g) b Source #
Supermap s t => Subeffect [Mapping Symbol *] Writer s t Source #
Methods sub :: s t a -> s g a Source #
type Unit [Mapping Symbol *] Writer Source #
type Unit [Mapping Symbol ] Writer = [] (Mapping Symbol )
type Plus [Mapping Symbol *] Writer s t Source #
type Plus [Mapping Symbol ] Writer s t = Union Symbol s t
type Inv [Mapping Symbol *] Writer s t Source #
type Inv [Mapping Symbol ] Writer s t = (IsMap Symbol s, IsMap Symbol * t, Unionable s t)

data Symbol :: * #

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

SingKind Symbol	Since: 4.9.0.0
Associated Types type DemoteRep Symbol :: * Methods fromSing :: Sing Symbol a -> DemoteRep Symbol
KnownSymbol a => SingI Symbol a	Since: 4.9.0.0
Methods sing :: Sing a a
FilterV f k v ([] (Mapping Symbol *))
Methods filterV :: Proxy Flag f -> Var k -> v -> Map [Mapping Symbol ] -> Map (Filter (Mapping Symbol ) f ((Symbol :-> ) k v) [Mapping Symbol ])
(Conder ((\|\|) ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) GT) ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) EQ)), FilterV FMax k v xs) => FilterV FMax k v ((:) (Mapping Symbol *) x xs)
Methods filterV :: Proxy Flag FMax -> Var k -> v -> Map ((Mapping Symbol * ': x) xs) -> Map (Filter (Mapping Symbol ) FMax ((Symbol :-> ) k v) ((Mapping Symbol * ': x) xs))
(Conder ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) LT), FilterV FMin k v xs) => FilterV FMin k v ((:) (Mapping Symbol *) x xs)
Methods filterV :: Proxy Flag FMin -> Var k -> v -> Map ((Mapping Symbol * ': x) xs) -> Map (Filter (Mapping Symbol ) FMin ((Symbol :-> ) k v) ((Mapping Symbol * ': x) xs))
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 ((:) (Mapping Symbol ) ((:->) Symbol v t) m)
Methods lookp :: Var v -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) m) -> t #
IsMember v t m => IsMember v t ((:) (Mapping Symbol *) x m)
Methods lookp :: Var v -> Map ((Mapping Symbol * ': x) m) -> t #
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) #
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) #
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 #
(KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((:) (Mapping Symbol ) ((:->) Symbol k v) s))
Methods show' :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> String
Show' (Map ([] (Mapping Symbol *)))
Methods show' :: Map [Mapping Symbol *] -> String
Sortable ([] (Mapping Symbol *))
Methods quicksort :: Map [Mapping Symbol ] -> Map (Sort (Mapping Symbol ) [Mapping Symbol *])
Nubable ([] (Mapping Symbol *))
Methods nub :: Map [Mapping Symbol ] -> Map (Nub Symbol [Mapping Symbol *]) #
CoeffectZip [Mapping Symbol *] IxCoreader Source #
Associated Types type Meet IxCoreader (c :: IxCoreader -> * -> ) (s :: IxCoreader) (t :: IxCoreader) :: k Source # type CzipInv IxCoreader (c :: IxCoreader -> -> *) (s :: IxCoreader) (t :: IxCoreader) :: Constraint Source # Methods czip :: CzipInv IxCoreader c s t => c s a -> c t b -> c (Meet IxCoreader c s t) (a, b) Source #
Coeffect [Mapping Symbol *] IxCoreader Source #
Associated Types type Inv IxCoreader (c :: IxCoreader -> * -> ) (s :: IxCoreader) (t :: IxCoreader) :: Constraint Source # type Unit IxCoreader (c :: IxCoreader -> -> ) :: k Source # type Plus IxCoreader (c :: IxCoreader -> -> *) (s :: IxCoreader) (t :: IxCoreader) :: k Source # Methods extract :: c (Unit IxCoreader c) a -> a Source # extend :: Inv IxCoreader c s t => (c t a -> b) -> c (Plus IxCoreader c s t) a -> c s b Source #
Effect [Mapping Symbol *] Reader Source #
Associated Types type Unit Reader (m :: Reader -> * -> ) :: k Source # type Plus Reader (m :: Reader -> -> ) (f :: Reader) (g :: Reader) :: k Source # type Inv Reader (m :: Reader -> -> *) (f :: Reader) (g :: Reader) :: Constraint Source # Methods return :: a -> m (Unit Reader m) a Source # (>>=) :: Inv Reader m f g => m f a -> (a -> m g b) -> m (Plus Reader m f g) b Source # (>>) :: Inv Reader m f g => m f a -> m g b -> m (Plus Reader m f g) b Source #
Effect [Mapping Symbol *] Writer Source #
Associated Types type Unit Writer (m :: Writer -> * -> ) :: k Source # type Plus Writer (m :: Writer -> -> ) (f :: Writer) (g :: Writer) :: k Source # type Inv Writer (m :: Writer -> -> *) (f :: Writer) (g :: Writer) :: Constraint Source # Methods return :: a -> m (Unit Writer m) a Source # (>>=) :: Inv Writer m f g => m f a -> (a -> m g b) -> m (Plus Writer m f g) b Source # (>>) :: Inv Writer m f g => m f a -> m g b -> m (Plus Writer m f g) b Source #
Submap s t => Subeffect [Mapping Symbol *] Reader s t Source #	If `s` is a subset of `t` then, `s` is a subeffect of `t`
Methods sub :: s t a -> s g a Source #
Supermap s t => Subeffect [Mapping Symbol *] Writer s t Source #
Methods sub :: s t a -> s g a Source #
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 *]) #
(Sortable (Filter (Mapping Symbol ) FMin ((:->) Symbol k v) xs), Sortable (Filter (Mapping Symbol ) FMax ((:->) Symbol k v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((:) (Mapping Symbol ) ((:->) Symbol k v) xs)
Methods quicksort :: Map ((Mapping Symbol * ': (Symbol :-> ) k v) xs) -> Map (Sort (Mapping Symbol ) ((Mapping Symbol * ': (Symbol :-> *) k v) xs))
(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))) #
Nubable ((:) (Mapping Symbol ) e ([] (Mapping Symbol )))
Methods nub :: Map ((Mapping Symbol * ': e) [Mapping Symbol ]) -> Map (Nub Symbol ((Mapping Symbol * ': e) [Mapping Symbol *])) #
((~) [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))) #
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)) #
data Sing Symbol
data Sing Symbol where SSym :: Sing Symbol s
type DemoteRep Symbol
type DemoteRep Symbol = String
type (==) Symbol a b
type (==) Symbol a b = EqSymbol a b
type Cmp Symbol k k'
type Cmp Symbol k k' = CmpSymbol k k'
type Unit [Mapping Symbol *] IxCoreader Source #
type Unit [Mapping Symbol ] IxCoreader = [] (Mapping Symbol )
type Unit [Mapping Symbol *] Reader Source #
type Unit [Mapping Symbol ] Reader = [] (Mapping Symbol )
type Unit [Mapping Symbol *] Writer Source #
type Unit [Mapping Symbol ] Writer = [] (Mapping Symbol )
type Meet [Mapping Symbol *] IxCoreader s t Source #
type Meet [Mapping Symbol ] IxCoreader s t = Union Symbol s t
type CzipInv [Mapping Symbol *] IxCoreader s t Source #
type CzipInv [Mapping Symbol *] IxCoreader s t = Unionable s t
type Inv [Mapping Symbol *] IxCoreader s t Source #
type Inv [Mapping Symbol ] IxCoreader s t = (Unionable s t, Split s t (Union Symbol s t))
type Plus [Mapping Symbol *] IxCoreader s t Source #
type Plus [Mapping Symbol ] IxCoreader s t = Union Symbol s t
type Plus [Mapping Symbol *] Reader f g Source #
type Plus [Mapping Symbol ] Reader f g = Union Symbol f g
type Plus [Mapping Symbol *] Writer s t Source #
type Plus [Mapping Symbol ] Writer s t = Union Symbol s t
type Inv [Mapping Symbol *] Reader f g Source #
type Inv [Mapping Symbol ] Reader f g = (IsMap Symbol f, IsMap Symbol * g, Split f g (Union Symbol * f g))
type Inv [Mapping Symbol *] Writer s t Source #
type Inv [Mapping Symbol ] Writer s t = (IsMap Symbol s, IsMap Symbol * t, Unionable s 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'

put :: Var v -> a -> Writer '[v :-> a] () Source #

Write to variable v with value of type a

data Mapping k v :: * -> * -> * #

A key-value pair

Constructors

k :-> v infixr 4

Instances

FilterV f k v ([] (Mapping Symbol *))
Methods filterV :: Proxy Flag f -> Var k -> v -> Map [Mapping Symbol ] -> Map (Filter (Mapping Symbol ) f ((Symbol :-> ) k v) [Mapping Symbol ])
(Conder ((\|\|) ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) GT) ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) EQ)), FilterV FMax k v xs) => FilterV FMax k v ((:) (Mapping Symbol *) x xs)
Methods filterV :: Proxy Flag FMax -> Var k -> v -> Map ((Mapping Symbol * ': x) xs) -> Map (Filter (Mapping Symbol ) FMax ((Symbol :-> ) k v) ((Mapping Symbol * ': x) xs))
(Conder ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) LT), FilterV FMin k v xs) => FilterV FMin k v ((:) (Mapping Symbol *) x xs)
Methods filterV :: Proxy Flag FMin -> Var k -> v -> Map ((Mapping Symbol * ': x) xs) -> Map (Filter (Mapping Symbol ) FMin ((Symbol :-> ) k v) ((Mapping Symbol * ': x) xs))
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 ((:) (Mapping Symbol ) ((:->) Symbol v t) m)
Methods lookp :: Var v -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) m) -> t #
IsMember v t m => IsMember v t ((:) (Mapping Symbol *) x m)
Methods lookp :: Var v -> Map ((Mapping Symbol * ': x) m) -> t #
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) #
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) #
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 #
(KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((:) (Mapping Symbol ) ((:->) Symbol k v) s))
Methods show' :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> String
Show' (Map ([] (Mapping Symbol *)))
Methods show' :: Map [Mapping Symbol *] -> String
Sortable ([] (Mapping Symbol *))
Methods quicksort :: Map [Mapping Symbol ] -> Map (Sort (Mapping Symbol ) [Mapping Symbol *])
Nubable ([] (Mapping Symbol *))
Methods nub :: Map [Mapping Symbol ] -> Map (Nub Symbol [Mapping Symbol *]) #
CoeffectZip [Mapping Symbol *] IxCoreader Source #
Associated Types type Meet IxCoreader (c :: IxCoreader -> * -> ) (s :: IxCoreader) (t :: IxCoreader) :: k Source # type CzipInv IxCoreader (c :: IxCoreader -> -> *) (s :: IxCoreader) (t :: IxCoreader) :: Constraint Source # Methods czip :: CzipInv IxCoreader c s t => c s a -> c t b -> c (Meet IxCoreader c s t) (a, b) Source #
Coeffect [Mapping Symbol *] IxCoreader Source #
Associated Types type Inv IxCoreader (c :: IxCoreader -> * -> ) (s :: IxCoreader) (t :: IxCoreader) :: Constraint Source # type Unit IxCoreader (c :: IxCoreader -> -> ) :: k Source # type Plus IxCoreader (c :: IxCoreader -> -> *) (s :: IxCoreader) (t :: IxCoreader) :: k Source # Methods extract :: c (Unit IxCoreader c) a -> a Source # extend :: Inv IxCoreader c s t => (c t a -> b) -> c (Plus IxCoreader c s t) a -> c s b Source #
Effect [Mapping Symbol *] Reader Source #
Associated Types type Unit Reader (m :: Reader -> * -> ) :: k Source # type Plus Reader (m :: Reader -> -> ) (f :: Reader) (g :: Reader) :: k Source # type Inv Reader (m :: Reader -> -> *) (f :: Reader) (g :: Reader) :: Constraint Source # Methods return :: a -> m (Unit Reader m) a Source # (>>=) :: Inv Reader m f g => m f a -> (a -> m g b) -> m (Plus Reader m f g) b Source # (>>) :: Inv Reader m f g => m f a -> m g b -> m (Plus Reader m f g) b Source #
Effect [Mapping Symbol *] Writer Source #
Associated Types type Unit Writer (m :: Writer -> * -> ) :: k Source # type Plus Writer (m :: Writer -> -> ) (f :: Writer) (g :: Writer) :: k Source # type Inv Writer (m :: Writer -> -> *) (f :: Writer) (g :: Writer) :: Constraint Source # Methods return :: a -> m (Unit Writer m) a Source # (>>=) :: Inv Writer m f g => m f a -> (a -> m g b) -> m (Plus Writer m f g) b Source # (>>) :: Inv Writer m f g => m f a -> m g b -> m (Plus Writer m f g) b Source #
Submap s t => Subeffect [Mapping Symbol *] Reader s t Source #	If `s` is a subset of `t` then, `s` is a subeffect of `t`
Methods sub :: s t a -> s g a Source #
Supermap s t => Subeffect [Mapping Symbol *] Writer s t Source #
Methods sub :: s t a -> s g a Source #
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 *]) #
(Sortable (Filter (Mapping Symbol ) FMin ((:->) Symbol k v) xs), Sortable (Filter (Mapping Symbol ) FMax ((:->) Symbol k v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((:) (Mapping Symbol ) ((:->) Symbol k v) xs)
Methods quicksort :: Map ((Mapping Symbol * ': (Symbol :-> ) k v) xs) -> Map (Sort (Mapping Symbol ) ((Mapping Symbol * ': (Symbol :-> *) k v) xs))
(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))) #
Nubable ((:) (Mapping Symbol ) e ([] (Mapping Symbol )))
Methods nub :: Map ((Mapping Symbol * ': e) [Mapping Symbol ]) -> Map (Nub Symbol ((Mapping Symbol * ': e) [Mapping Symbol *])) #
((~) [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))) #
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 Unit [Mapping Symbol *] IxCoreader Source #
type Unit [Mapping Symbol ] IxCoreader = [] (Mapping Symbol )
type Unit [Mapping Symbol *] Reader Source #
type Unit [Mapping Symbol ] Reader = [] (Mapping Symbol )
type Unit [Mapping Symbol *] Writer Source #
type Unit [Mapping Symbol ] Writer = [] (Mapping Symbol )
type Meet [Mapping Symbol *] IxCoreader s t Source #
type Meet [Mapping Symbol ] IxCoreader s t = Union Symbol s t
type CzipInv [Mapping Symbol *] IxCoreader s t Source #
type CzipInv [Mapping Symbol *] IxCoreader s t = Unionable s t
type Inv [Mapping Symbol *] IxCoreader s t Source #
type Inv [Mapping Symbol ] IxCoreader s t = (Unionable s t, Split s t (Union Symbol s t))
type Plus [Mapping Symbol *] IxCoreader s t Source #
type Plus [Mapping Symbol ] IxCoreader s t = Union Symbol s t
type Plus [Mapping Symbol *] Reader f g Source #
type Plus [Mapping Symbol ] Reader f g = Union Symbol f g
type Plus [Mapping Symbol *] Writer s t Source #
type Plus [Mapping Symbol ] Writer s t = Union Symbol s t
type Inv [Mapping Symbol *] Reader f g Source #
type Inv [Mapping Symbol ] Reader f g = (IsMap Symbol f, IsMap Symbol * g, Split f g (Union Symbol * f g))
type Inv [Mapping Symbol *] Writer s t Source #
type Inv [Mapping Symbol ] Writer s t = (IsMap Symbol s, IsMap Symbol * t, Unionable s 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 IsMap k v (s :: [Mapping k v]) = (~) [Mapping k v] s (Nub k v (Sort (Mapping k v) s)) #

Predicate to check if in normalised map form

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

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

Constructors

Empty :: Map ([] (Mapping Symbol *))
Ext :: Map ((:) (Mapping Symbol ) ((:->) Symbol 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 #
(KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((:) (Mapping Symbol ) ((:->) Symbol k v) s))
Methods show' :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> String
Show' (Map ([] (Mapping Symbol *)))
Methods show' :: Map [Mapping Symbol *] -> String

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

Union of two finite maps (normalising)

data Var (k :: Symbol) :: 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 #

type Union k v (m :: [Mapping k v]) (n :: [Mapping k v]) = Nub k v (Sort (Mapping k v) ((:++) (Mapping k v) m n)) #

Union of two finite maps

type Unionable (s :: [Mapping Symbol *]) (t :: [Mapping Symbol *]) = (Nubable (Sort (Mapping Symbol *) ((:++) (Mapping Symbol *) s t)), Sortable ((:++) (Mapping Symbol *) s t)) #

Orphan instances

(Monoid u, Nubable ((:) (Mapping Symbol ) ((:->) Symbol k u) s)) => Nubable ((:) (Mapping Symbol ) ((:->) Symbol k u) ((:) (Mapping Symbol ) ((:->) Symbol k u) s)) Source #	Define the operation for removing duplicates using mappend
Methods nub :: Map ((Mapping Symbol * ': (Symbol :-> ) k u) ((Mapping Symbol ': (Symbol :-> ) k u) s)) -> Map (Nub Symbol ((Mapping Symbol * ': (Symbol :-> ) k u) ((Mapping Symbol ': (Symbol :-> *) k u) s))) #

FilterV f k v ([] (Mapping Symbol *))
Methods filterV :: Proxy Flag f -> Var k -> v -> Map [Mapping Symbol ] -> Map (Filter (Mapping Symbol ) f ((Symbol :-> ) k v) [Mapping Symbol ])
(Conder ((\|\|) ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) GT) ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) EQ)), FilterV FMax k v xs) => FilterV FMax k v ((:) (Mapping Symbol *) x xs)
Methods filterV :: Proxy Flag FMax -> Var k -> v -> Map ((Mapping Symbol * ': x) xs) -> Map (Filter (Mapping Symbol ) FMax ((Symbol :-> ) k v) ((Mapping Symbol * ': x) xs))
(Conder ((==) Ordering (Cmp (Mapping Symbol ) x ((:->) Symbol k v)) LT), FilterV FMin k v xs) => FilterV FMin k v ((:) (Mapping Symbol *) x xs)
Methods filterV :: Proxy Flag FMin -> Var k -> v -> Map ((Mapping Symbol * ': x) xs) -> Map (Filter (Mapping Symbol ) FMin ((Symbol :-> ) k v) ((Mapping Symbol * ': x) xs))
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 ((:) (Mapping Symbol ) ((:->) Symbol v t) m)
Methods lookp :: Var v -> Map ((Mapping Symbol * ': (Symbol :-> *) v t) m) -> t #
IsMember v t m => IsMember v t ((:) (Mapping Symbol *) x m)
Methods lookp :: Var v -> Map ((Mapping Symbol * ': x) m) -> t #
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) #
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) #
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 #
(KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((:) (Mapping Symbol ) ((:->) Symbol k v) s))
Methods show' :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> String
Show' (Map ([] (Mapping Symbol *)))
Methods show' :: Map [Mapping Symbol *] -> String
Sortable ([] (Mapping Symbol *))
Methods quicksort :: Map [Mapping Symbol ] -> Map (Sort (Mapping Symbol ) [Mapping Symbol *])
Nubable ([] (Mapping Symbol *))
Methods nub :: Map [Mapping Symbol ] -> Map (Nub Symbol [Mapping Symbol *]) #
CoeffectZip [Mapping Symbol *] IxCoreader Source #
Associated Types type Meet IxCoreader (c :: IxCoreader -> * -> ) (s :: IxCoreader) (t :: IxCoreader) :: k Source # type CzipInv IxCoreader (c :: IxCoreader -> -> *) (s :: IxCoreader) (t :: IxCoreader) :: Constraint Source # Methods czip :: CzipInv IxCoreader c s t => c s a -> c t b -> c (Meet IxCoreader c s t) (a, b) Source #
Coeffect [Mapping Symbol *] IxCoreader Source #
Associated Types type Inv IxCoreader (c :: IxCoreader -> * -> ) (s :: IxCoreader) (t :: IxCoreader) :: Constraint Source # type Unit IxCoreader (c :: IxCoreader -> -> ) :: k Source # type Plus IxCoreader (c :: IxCoreader -> -> *) (s :: IxCoreader) (t :: IxCoreader) :: k Source # Methods extract :: c (Unit IxCoreader c) a -> a Source # extend :: Inv IxCoreader c s t => (c t a -> b) -> c (Plus IxCoreader c s t) a -> c s b Source #
Effect [Mapping Symbol *] Reader Source #
Associated Types type Unit Reader (m :: Reader -> * -> ) :: k Source # type Plus Reader (m :: Reader -> -> ) (f :: Reader) (g :: Reader) :: k Source # type Inv Reader (m :: Reader -> -> *) (f :: Reader) (g :: Reader) :: Constraint Source # Methods return :: a -> m (Unit Reader m) a Source # (>>=) :: Inv Reader m f g => m f a -> (a -> m g b) -> m (Plus Reader m f g) b Source # (>>) :: Inv Reader m f g => m f a -> m g b -> m (Plus Reader m f g) b Source #
Effect [Mapping Symbol *] Writer Source #
Associated Types type Unit Writer (m :: Writer -> * -> ) :: k Source # type Plus Writer (m :: Writer -> -> ) (f :: Writer) (g :: Writer) :: k Source # type Inv Writer (m :: Writer -> -> *) (f :: Writer) (g :: Writer) :: Constraint Source # Methods return :: a -> m (Unit Writer m) a Source # (>>=) :: Inv Writer m f g => m f a -> (a -> m g b) -> m (Plus Writer m f g) b Source # (>>) :: Inv Writer m f g => m f a -> m g b -> m (Plus Writer m f g) b Source #
Submap s t => Subeffect [Mapping Symbol *] Reader s t Source #	If `s` is a subset of `t` then, `s` is a subeffect of `t`
Methods sub :: s t a -> s g a Source #
Supermap s t => Subeffect [Mapping Symbol *] Writer s t Source #
Methods sub :: s t a -> s g a Source #
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 *]) #
(Sortable (Filter (Mapping Symbol ) FMin ((:->) Symbol k v) xs), Sortable (Filter (Mapping Symbol ) FMax ((:->) Symbol k v) xs), FilterV FMin k v xs, FilterV FMax k v xs) => Sortable ((:) (Mapping Symbol ) ((:->) Symbol k v) xs)
Methods quicksort :: Map ((Mapping Symbol * ': (Symbol :-> ) k v) xs) -> Map (Sort (Mapping Symbol ) ((Mapping Symbol * ': (Symbol :-> *) k v) xs))
(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))) #
Nubable ((:) (Mapping Symbol ) e ([] (Mapping Symbol )))
Methods nub :: Map ((Mapping Symbol * ': e) [Mapping Symbol ]) -> Map (Nub Symbol ((Mapping Symbol * ': e) [Mapping Symbol *])) #
((~) [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))) #
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 Unit [Mapping Symbol *] IxCoreader Source #
type Unit [Mapping Symbol ] IxCoreader = [] (Mapping Symbol )
type Unit [Mapping Symbol *] Reader Source #
type Unit [Mapping Symbol ] Reader = [] (Mapping Symbol )
type Unit [Mapping Symbol *] Writer Source #
type Unit [Mapping Symbol ] Writer = [] (Mapping Symbol )
type Meet [Mapping Symbol *] IxCoreader s t Source #
type Meet [Mapping Symbol ] IxCoreader s t = Union Symbol s t
type CzipInv [Mapping Symbol *] IxCoreader s t Source #
type CzipInv [Mapping Symbol *] IxCoreader s t = Unionable s t
type Inv [Mapping Symbol *] IxCoreader s t Source #
type Inv [Mapping Symbol ] IxCoreader s t = (Unionable s t, Split s t (Union Symbol s t))
type Plus [Mapping Symbol *] IxCoreader s t Source #
type Plus [Mapping Symbol ] IxCoreader s t = Union Symbol s t
type Plus [Mapping Symbol *] Reader f g Source #
type Plus [Mapping Symbol ] Reader f g = Union Symbol f g
type Plus [Mapping Symbol *] Writer s t Source #
type Plus [Mapping Symbol ] Writer s t = Union Symbol s t
type Inv [Mapping Symbol *] Reader f g Source #
type Inv [Mapping Symbol ] Reader f g = (IsMap Symbol f, IsMap Symbol * g, Split f g (Union Symbol * f g))
type Inv [Mapping Symbol *] Writer s t Source #
type Inv [Mapping Symbol ] Writer s t = (IsMap Symbol s, IsMap Symbol * t, Unionable s 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'

(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 #
(KnownSymbol k, Show v, Show' (Map s)) => Show' (Map ((:) (Mapping Symbol ) ((:->) Symbol k v) s))
Methods show' :: Map ((Mapping Symbol * ': (Symbol :-> *) k v) s) -> String
Show' (Map ([] (Mapping Symbol *)))
Methods show' :: Map [Mapping Symbol *] -> String