ixmonad-0.56: Embeds effect systems into Haskell using parameteric effect monads

Safe HaskellNone
LanguageHaskell98

Control.Effect.State

Synopsis

Documentation

data Set n where Source

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 Source

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

put :: Var v -> a -> State `[k :-> (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 infixl 2 Source

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

Distinguish reads, writes, and read-writes |

Constructors

R 
W 
RW 

data Action s Source

Provides a wrapper for effect actions |

Constructors

Eff 

Instances

data Var k where Source

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

type Sortable s = Bubbler s s Source

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 t v Source

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 Source

class Split s t st Source

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)