Safe Haskell | None |
---|---|
Language | Haskell98 |
- data Set k (n :: [k]) :: forall k. [k] -> * where
- get :: Var v -> State '[v :-> (a :! R)] a
- put :: Var v -> a -> State '[v :-> (a :! W)] ()
- data State s a = State {}
- data (k :: Symbol) :-> (v :: *) = (Var k) :-> v
- data a :! (s :: Eff) = a :! (Action s)
- data Eff
- data Action (s :: Eff) = Eff
- data Var (k :: Symbol) where
- union :: Unionable s t => Set s -> Set t -> Set (UnionS s t)
- type UnionS s t = Nub (Sort (s :++ t))
- type family Reads t where ...
- type family Writes t where ...
- type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)) (Nub (Sort (s :++ t))), Split s t (Union s t))
- class Sortable k (xs :: [k])
- type SetLike s = Nub (Sort s)
- type StateSet f = (StateSetProperties f, StateSetProperties (Reads f), StateSetProperties (Writes f))
- type IntersectR s t = (Sortable (s :++ t), Update (Sort (s :++ t)) t)
- class Update s t
- type family Sort k (xs :: [k]) :: [k] where ...
- class Split k k1 k2 (s :: [k]) (t :: [k1]) (st :: [k2])
Documentation
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
Parametric effect state monad
data (k :: Symbol) :-> (v :: *) infixl 2 Source #
Update * k ((:) * ((:->) u ((:!) b s)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as' Source # | |
Update * k ((:) * ((:->) v ((:!) a R)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as' Source # | |
Update * * ((:) * ((:->) u ((:!) b s)) as) as' => Update * * ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as') Source # | |
(Show (Var k), Show v) => Show ((:->) k v) Source # | |
type Cmp * ((:->) v a) ((:->) u b) Source # | |
data a :! (s :: Eff) infixl 3 Source #
Describes an effect action s
on a value of type a
Update * k ((:) * ((:->) u ((:!) b s)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as' Source # | |
Update * k ((:) * ((:->) v ((:!) a R)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as' Source # | |
Update * * ((:) * ((:->) u ((:!) b s)) as) as' => Update * * ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as') Source # | |
(Show (Action f), Show a) => Show ((:!) a f) 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
union :: Unionable s t => Set s -> Set t -> Set (UnionS s t) Source #
Union operation for state effects
type Unionable s t = (Sortable (s :++ t), Nubable (Sort (s :++ t)) (Nub (Sort (s :++ t))), Split s t (Union s t)) Source #
type StateSet f = (StateSetProperties f, StateSetProperties (Reads f), StateSetProperties (Writes f)) Source #
Captures what it means to be a set of state effects
Update reads, that is any writes are pushed into reads, a bit like intersection
update
Update k2 k1 xs ([] k1) Source # | |
Update k k ((:) k e ([] k)) ((:) k e ([] k)) Source # | |
Update * k ((:) * ((:->) u ((:!) b s)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) u ((:!) b s)) as)) as' Source # | |
Update * k ((:) * ((:->) v ((:!) a R)) as) as' => Update * k ((:) * ((:->) v ((:!) a W)) ((:) * ((:->) v ((:!) b R)) as)) as' Source # | |
Update * * ((:) * ((:->) u ((:!) b s)) as) as' => Update * * ((:) * ((:->) v ((:!) a R)) ((:) * ((:->) u ((:!) b s)) as)) ((:) * ((:->) v ((:!) a R)) as') Source # | |
type family Sort k (xs :: [k]) :: [k] where ... #
Type-level quick sort for normalising the representation of sets