Safe Haskell	None
Language	Haskell98

Control.Effect.State

Synopsis

Documentation

data Set n :: [*] -> * where

Constructors

Empty :: Set ([] *)
Ext :: e -> Set s -> Set ((:) * e s)

Instances

(Show e, Show' (Set s)) => Show (Set ((:) * e s))
Show (Set ([] *))
(Show' (Set s), Show e) => Show' (Set ((:) * e s))
Show' (Set ([] *))

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
type Unit [] State = []
type Plus [*] State s t = UnionS s t
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 :-> v :: Symbol -> * -> *

Constructors

(Var k) :-> v

Instances

(Show (Var k), Show v) => Show ((:->) k v)
(Monoid u, Nubable ((:) * ((:->) k u) s)) => Nubable ((:) * ((:->) k u) ((:) * ((:->) k u) s))	Define the operation for removing duplicates using mappend
Update ((:) * ((:->) u ((:!) b s)) as) as' => Update ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as'
Update ((:) * ((:->) v ((:!) a R)) as) as' => Update ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as'
Update ((:) * ((:->) u ((:!) b s)) as) as' => Update ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as')
type Cmp * ((:->) v a) ((:->) u b) = CmpSymbol v u

data a :! s infixl 3 Source

Describes an effect action s on a value of type a

Constructors

a :! (Action s) infixl 3

Instances

(Show (Action f), Show a) => Show ((:!) a f)
Update ((:) * ((:->) u ((:!) b s)) as) as' => Update ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as'
Update ((:) * ((:->) v ((:!) a R)) as) as' => Update ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as'
Update ((:) * ((:->) u ((:!) b s)) as) as' => Update ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as')

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 Source

Provides a wrapper for effect actions

Constructors

Eff

Instances

Show (Action RW)
Show (Action W)
Show (Action R)

data Var k :: Symbol -> * where

Constructors

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

Instances

Show (Var v)
Show (Var "x")
Show (Var "y")
Show (Var "z")

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

Union operation for state effects

type UnionS s t = Nub (Sort (Append s t)) Source

type family Reads t 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 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 (Append s t), Nubable (Sort (Append s t)) (Nub (Sort (Append s t))), Split s t (Union s t)) Source

class Sortable xs

Minimal complete definition

quicksort

Instances

Sortable ([] *)
(Sortable (Filter * FMin p xs), Sortable (Filter * FMax p xs), FilterV FMin p xs, FilterV FMax p xs) => Sortable ((:) * p 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 (Append s t), Update (Sort (Append 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 xs ([] *)
Update ((:) * ((:->) u ((:!) b s)) as) as' => Update ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as'
Update ((:) * ((:->) v ((:!) a R)) as) as' => Update ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as'
Update ((:) * e ([] )) ((:) e ([] *))
Update ((:) * ((:->) u ((:!) b s)) as) as' => Update ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as')

type family Sort xs :: [k]

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 s t st

Minimal complete definition

split

Instances

Split s t st => Split s ((:) * x t) ((:) * x st)
Split ([] ) ([] ) ([] *)
Split s t st => Split ((:) * x s) t ((:) * x st)
Split s t st => Split ((:) * x s) ((:) * x t) ((:) * x st)