state

For a state: one value, got and put.

StateF

data StateF s (m : Type -> Type) x = Get (s -> x) | Put s x

The operations: each says what it gives back by a function to the rest (x).

state

state : (s : Type) -> HFunctor

For one value read and replaced along a computation.

get

get : {s : Type} -> {e : HFunctor} -> {{ev : state s <: e}} -> Co e s

The value, got: in any effect the state is in, by the evidence.

put

put : {s : Type} -> {e : HFunctor} -> {{ev : state s <: e}} -> s -> Co e Unit

… and put.

statefulFunctor

statefulFunctor : (s : Type) -> (e : HFunctor) -> RawFunctor

stateful

stateful : (s : Type) -> (e : HFunctor) -> Handler (state s <+> e)

A handler of state s into the rest of the world, e: the state threaded from each operation to the next. An operation of e’s is done as it is; one that holds a computation of its own runs it from the state there, and what that run leaves of the state is not kept.

runState

runState : {s : Type}
         -> {e : HFunctor}
         -> {a : Type}
         -> s
         -> Co (state s <+> e) a
         -> Co e (a, s)

c from the state s0: what it comes to, and the state it leaves.