git.iko.soy/Idris-dev
on bfa39bf help sign in
Idris-dev/effects/Effect/State.idr
40 lines 830 B history raw
1module Effect.State
3import Effects
5%access public
7data State : Effect where
8 Get : State a a a
9 Put : b -> State a b ()
11using (m : Type -> Type)
12 instance Handler State m where
13 handle st Get k = k st st
14 handle st (Put n) k = k n ()
16STATE : Type -> EFFECT
17STATE t = MkEff t State
19get : Eff m [STATE x] x
20get = Get
22put : x -> Eff m [STATE x] ()
23put val = Put val
25putM : y -> EffM m [STATE x] [STATE y] ()
26putM val = Put val
28update : (x -> x) -> Eff m [STATE x] ()
29update f = put (f !get)
31updateM : (x -> y) -> EffM m [STATE x] [STATE y] ()
32updateM f = putM (f !get)
34locally : x -> Eff m [STATE x] t -> Eff m [STATE y] t
35locally newst prog = do st <- get
36 putM newst
37 val <- prog
38 putM st
39 return val