effect-monad-0.6: Embeds effect systems into Haskell using parameteric effect monads

Safe HaskellNone
LanguageHaskell98

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 `[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 :: 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

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)