--State2 effect effect State se2 where put : ∀ se . se -> {State se} () get : ∀ se . () -> {State se} se state : ∀ s a . s -> Effect (State s) a -> (s, a) state woot eff = case eff of { State.get () -> k } -> handle (state woot) in (k woot) { State.put snew -> k } -> handle (state snew) in (k ()) { a } -> (woot, a) ()