Control.Effect.State

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

get :: Var v -> State `[v :-> (a :! R)]` a

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

put :: Var v -> a -> State `[k :-> (a :! W)]` ()

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

data State s a

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 infixl 2

Constructors

(Var k) :-> v infixl 2

Instances

(Show (Var k), Show v) => Show ((:->) k v)

Chooser (CmpSymbol j k) => OrdH ((:->) j u) ((:->) k v)

(Monoid u, Nubable ((:) * ((:->) k u) s)) => Nubable ((:) * ((:->) k u) ((:) * ((:->) k u) s))

Define the operation for removing duplicates using mappend |

Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) j ((:!) b s)) as)) as'

Update ((:) * ((:->) k ((:!) a R)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) k ((:!) b R)) as)) as'

Update ((:) * ((:->) k ((:!) b R)) as) as' => Update ((:) * ((:->) k ((:!) a s)) ((:) * ((:->) k ((:!) b s)) as)) as'

Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a R)) ((:) * ((:->) j ((:!) b s)) as)) ((:) * ((:->) k ((:!) a R)) as')

type Max ((:->) j u) ((:->) k v) = (:->) (Select Symbol j k k j) (Select * j k v u)

type Min ((:->) j u) ((:->) k v) = (:->) (Select Symbol j k j k) (Select * j k u v)

data a :! s infixl 3

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 ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) j ((:!) b s)) as)) as'

Update ((:) * ((:->) k ((:!) a R)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) k ((:!) b R)) as)) as'

Update ((:) * ((:->) k ((:!) b R)) as) as' => Update ((:) * ((:->) k ((:!) a s)) ((:) * ((:->) k ((:!) b s)) as)) as'

Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a R)) ((:) * ((:->) j ((:!) b s)) as)) ((:) * ((:->) k ((:!) a R)) as')

data Eff

Distinguish reads, writes, and read-writes |

Constructors

R

W

RW

data Action s

Provides a wrapper for effect actions |

Constructors

Eff

Instances

Show (Action RW)

Show (Action W)

Show (Action R)

data Var k where

Constructors

Var :: Var k

X :: Var "x"

Y :: Var "y"

Z :: Var "z"

Instances

Show (Var "x")

Show (Var "y")

Show (Var "z")

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

Union operation for state effects |

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

type family Reads t

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

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

type Sortable s = Bubbler s s

type SetLike s = Nub (Sort s)

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

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)

class Update t v

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

Minimal complete definition

update

Instances

Update xs ([] *)

Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) j ((:!) b s)) as)) as'

Update ((:) * ((:->) k ((:!) a R)) as) as' => Update ((:) * ((:->) k ((:!) a W)) ((:) * ((:->) k ((:!) b R)) as)) as'

Update ((:) * ((:->) k ((:!) b R)) as) as' => Update ((:) * ((:->) k ((:!) a s)) ((:) * ((:->) k ((:!) b s)) as)) as'

Update ((:) * e ([] *)) ((:) * e ([] *))

Update ((:) * ((:->) j ((:!) b s)) as) as' => Update ((:) * ((:->) k ((:!) a R)) ((:) * ((:->) j ((:!) b s)) as)) ((:) * ((:->) k ((:!) a R)) as')

type Sort l = Bubble l l

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)