effect-monad-0.8.1.0: Embeds effect systems and program logics into Haskell using graded monads and parameterised monads

Safe HaskellNone
LanguageHaskell98

Control.Effect.Reader

Synopsis

Documentation

newtype Reader (s :: [Mapping Symbol *]) a Source #

Provides a effect-parameterised version of the class reader monad. Effects are sets of variable-type pairs, providing an effect system for reader effects.

Constructors

IxR 

Fields

Instances

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 #

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 #

type Unit [Mapping Symbol *] Reader Source # 
type Plus [Mapping Symbol *] Reader f g Source # 
type Plus [Mapping Symbol *] Reader f g = Union Symbol * f g
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))

ask :: Var v -> Reader '[v :-> a] a Source #

ask for a variable v of type a, raising an effect

merge :: Unionable s t => (a -> Reader (Union s t) b) -> Reader s (a -> Reader t b) Source #

Provides a way to emulated the ImplicitParams features of GHC/Haskell

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 *))) 
(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 *))) 
(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 *)) 
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 *)) 
Split ([] (Mapping Symbol *)) ([] (Mapping Symbol *)) ([] (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 *] Reader Source # 
type Unit [Mapping Symbol *] Writer Source # 
type Meet [Mapping Symbol *] IxCoreader s t Source # 
type CzipInv [Mapping Symbol *] IxCoreader s t Source # 
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 *] 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 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'

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 #

class Submap (s :: [Mapping Symbol *]) (t :: [Mapping Symbol *]) #

Construct a submap s from a supermap t

Minimal complete definition

submap

Instances

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

Methods

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

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

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