Safe Haskell	None
Language	Haskell98

Control.Effect.State

Synopsis

Documentation

data Set k (n :: [k]) :: forall k. [k] -> * where #

Constructors

Empty :: Set k ([] k)
Ext :: Set * ((:) * e s)

Instances

(Eq e, Eq (Set * s)) => Eq (Set * ((:) * e s))
Methods (==) :: Set * ((* ': e) s) -> Set * ((* ': e) s) -> Bool # (/=) :: Set * ((* ': e) s) -> Set * ((* ': e) s) -> Bool #
(Show e, Show' (Set * s)) => Show (Set * ((:) * e s))
Methods showsPrec :: Int -> Set * ((* ': e) s) -> ShowS # show :: Set * ((* ': e) s) -> String # showList :: [Set * ((* ': e) s)] -> ShowS #
Show (Set k ([] k))
Methods showsPrec :: Int -> Set k [k] -> ShowS # show :: Set k [k] -> String # showList :: [Set k [k]] -> ShowS #
(Show' (Set * s), Show e) => Show' (Set * ((:) * e s))
Methods show' :: Set * ((* ': e) s) -> String
Show' (Set k ([] k))
Methods show' :: Set k [k] -> String

get :: Var v -> State '[v :-> (a :! R)] a Source #

Read from a variable v of type a. Raise a read effect.

put :: Var v -> a -> State '[v :-> (a :! W)] () Source #

Write to a variable v with a value of type a. Raises a write effect

data State s a Source #

Parametric effect state monad

Constructors

State
Fields runState :: Set (Reads s) -> (a, Set (Writes s))

Instances

Effect [*] State Source #
Associated Types type Unit State (m :: State -> * -> ) :: k Source # type Plus State (m :: State -> -> ) (f :: State) (g :: State) :: k Source # type Inv State (m :: State -> -> *) (f :: State) (g :: State) :: Constraint Source # Methods return :: a -> m (Unit State m) a Source # (>>=) :: Inv State m f g => m f a -> (a -> m g b) -> m (Plus State m f g) b Source # (>>) :: Inv State m f g => m f a -> m g b -> m (Plus State m f g) b Source #
type Unit [*] State Source #
type Unit [] State = []
type Plus [*] State s t Source #
type Plus [*] State s t = UnionS s t
type Inv [*] State s t Source #
type Inv [] State s t = (IsSet s, IsSet * (Reads s), IsSet * (Writes s), IsSet * t, IsSet * (Reads t), IsSet * (Writes t), (~) [] (Reads (Reads t)) (Reads t), (~) [] (Writes (Writes s)) (Writes s), Split * * * (Reads s) (Reads t) (Reads (UnionS s t)), Unionable (Writes s) (Writes t), IntersectR * (Writes s) (Reads t), (~) [*] (Writes (UnionS s t)) (UnionS (Writes s) (Writes t)))

data (k :: Symbol) :-> (v :: *) infixl 2 Source #

Constructors

(Var k) :-> v infixl 2

Instances

Update * k ((:) * ((:->) u ((:!) b s)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as' Source #
Methods update :: Set ((* ': (v :-> (a :! W))) ((* ': (u :-> (b :! s))) as)) s -> Set as' t
Update * k ((:) * ((:->) v ((:!) a R)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as' Source #
Methods update :: Set ((* ': (v :-> (a :! W))) ((* ': (v :-> (b :! R))) as)) s -> Set as' t
Update * * ((:) * ((:->) u ((:!) b s)) as) as' => Update * * ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as') Source #
Methods update :: Set ((* ': (v :-> (a :! R))) ((* ': (u :-> (b :! s))) as)) s -> Set ((* ': (v :-> (a :! R))) as') t
(Show (Var k), Show v) => Show ((:->) k v) Source #
Methods showsPrec :: Int -> (k :-> v) -> ShowS # show :: (k :-> v) -> String # showList :: [k :-> v] -> ShowS #
type Cmp * ((:->) v a) ((:->) u b) Source #
type Cmp * ((:->) v a) ((:->) u b) = CmpSymbol v u

data a :! (s :: Eff) infixl 3 Source #

Describes an effect action s on a value of type a

Constructors

a :! (Action s) infixl 3

Instances

Update * k ((:) * ((:->) u ((:!) b s)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as' Source #
Methods update :: Set ((* ': (v :-> (a :! W))) ((* ': (u :-> (b :! s))) as)) s -> Set as' t
Update * k ((:) * ((:->) v ((:!) a R)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as' Source #
Methods update :: Set ((* ': (v :-> (a :! W))) ((* ': (v :-> (b :! R))) as)) s -> Set as' t
Update * * ((:) * ((:->) u ((:!) b s)) as) as' => Update * * ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as') Source #
Methods update :: Set ((* ': (v :-> (a :! R))) ((* ': (u :-> (b :! s))) as)) s -> Set ((* ': (v :-> (a :! R))) as') t
(Show (Action f), Show a) => Show ((:!) a f) Source #
Methods showsPrec :: Int -> (a :! f) -> ShowS # show :: (a :! f) -> String # showList :: [a :! f] -> ShowS #

data Eff Source #

Provides an effect-parameterised version of the state monad, which gives an effect system for stateful computations with annotations that are sets of variable-type-action triples.

Distinguish reads, writes, and read-writes

Constructors

R
W
RW

data Action (s :: Eff) Source #

Provides a wrapper for effect actions

Constructors

Eff

Instances

Show (Action R) Source #
Methods showsPrec :: Int -> Action R -> ShowS # show :: Action R -> String # showList :: [Action R] -> ShowS #
Show (Action W) Source #
Methods showsPrec :: Int -> Action W -> ShowS # show :: Action W -> String # showList :: [Action W] -> ShowS #
Show (Action RW) Source #
Methods showsPrec :: Int -> Action RW -> ShowS # show :: Action RW -> String # showList :: [Action RW] -> ShowS #

data Var (k :: Symbol) where Source #

Constructors

Var :: Var k
X :: Var "x"
Y :: Var "y"
Z :: Var "z"

Instances

Show (Var v) Source #
Methods showsPrec :: Int -> Var v -> ShowS # show :: Var v -> String # showList :: [Var v] -> ShowS #
Show (Var "x") Source #
Methods showsPrec :: Int -> Var "x" -> ShowS # show :: Var "x" -> String # showList :: [Var "x"] -> ShowS #
Show (Var "y") Source #
Methods showsPrec :: Int -> Var "y" -> ShowS # show :: Var "y" -> String # showList :: [Var "y"] -> ShowS #
Show (Var "z") Source #
Methods showsPrec :: Int -> Var "z" -> ShowS # show :: Var "z" -> String # showList :: [Var "z"] -> ShowS #

union :: Unionable s t => Set s -> Set t -> Set (UnionS s t) Source #

Union operation for state effects

type UnionS s t = Nub (Sort (s :++ t)) Source #

type family Reads t where ... Source #

Calculate just the reader effects

Equations

Reads '[] = '[]
Reads ((k :-> (a :! R)) ': xs) = (k :-> (a :! R)) ': Reads xs
Reads ((k :-> (a :! RW)) ': xs) = (k :-> (a :! R)) ': Reads xs
Reads ((k :-> (a :! W)) ': xs) = Reads xs

type family Writes t where ... Source #

Calculate just the writer effects

Equations

Writes '[] = '[]
Writes ((k :-> (a :! W)) ': xs) = (k :-> (a :! W)) ': Writes xs
Writes ((k :-> (a :! RW)) ': xs) = (k :-> (a :! W)) ': Writes xs
Writes ((k :-> (a :! R)) ': xs) = Writes xs

type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)) (Nub (Sort (s :++ t))), Split s t (Union s t)) Source #

class Sortable k (xs :: [k]) #

Value-level quick sort that respects the type-level ordering

Minimal complete definition

quicksort

Instances

Sortable k ([] k)
Methods quicksort :: Set [k] xs -> Set [k] (Sort [k] xs) #
(Sortable * (Filter * FMin p xs), Sortable * (Filter * FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable * ((:) * p xs)
Methods quicksort :: Set ((* ': p) xs) xs -> Set ((* ': p) xs) (Sort ((* ': p) xs) xs) #

type SetLike s = Nub (Sort s) Source #

type StateSet f = (StateSetProperties f, StateSetProperties (Reads f), StateSetProperties (Writes f)) Source #

Captures what it means to be a set of state effects

type IntersectR s t = (Sortable (s :++ t), Update (Sort (s :++ t)) t) Source #

class Update s t Source #

Update reads, that is any writes are pushed into reads, a bit like intersection

Minimal complete definition

update

Instances

Update k2 k1 xs ([] k1) Source #
Methods update :: Set xs s -> Set [k1] t
Update k k ((:) k e ([] k)) ((:) k e ([] k)) Source #
Methods update :: Set ((k ': e) [k]) s -> Set ((k ': e) [k]) t
Update * k ((:) * ((:->) u ((:!) b s)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as' Source #
Methods update :: Set ((* ': (v :-> (a :! W))) ((* ': (u :-> (b :! s))) as)) s -> Set as' t
Update * k ((:) * ((:->) v ((:!) a R)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as' Source #
Methods update :: Set ((* ': (v :-> (a :! W))) ((* ': (v :-> (b :! R))) as)) s -> Set as' t
Update * * ((:) * ((:->) u ((:!) b s)) as) as' => Update * * ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as') Source #
Methods update :: Set ((* ': (v :-> (a :! R))) ((* ': (u :-> (b :! s))) as)) s -> Set ((* ': (v :-> (a :! R))) as') t

type family Sort k (xs :: [k]) :: [k] where ... #

Type-level quick sort for normalising the representation of sets

Equations

Sort k ([] k) = [] k
Sort k ((:) k x xs) = (:++) k ((:++) k (Sort k (Filter k FMin x xs)) ((:) k x ([] k))) (Sort k (Filter k FMax x xs))

class Split k k1 k2 (s :: [k]) (t :: [k1]) (st :: [k2]) #

Splitting a union a set, given the sets we want to split it into

Minimal complete definition

split

Instances

Split k2 k1 k1 s t st => Split k2 k1 k1 s ((:) k1 x t) ((:) k1 x st)
Methods split :: Set ((k1 ': x) st) st -> (Set s s, Set ((k1 ': x) t) t) #
Split k1 k2 k3 ([] k1) ([] k2) ([] k3)
Methods split :: Set [k3] st -> (Set [k1] s, Set [k2] t) #
Split k2 k1 k2 s t st => Split k2 k1 k2 ((:) k2 x s) t ((:) k2 x st)
Methods split :: Set ((k2 ': x) st) st -> (Set ((k2 ': x) s) s, Set t t) #
Split k k k s t st => Split k k k ((:) k x s) ((:) k x t) ((:) k x st)
Methods split :: Set ((k ': x) st) st -> (Set ((k ': x) s) s, Set ((k ': x) t) t) #