git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/effects/Effect/State.idr
40 lines 839 B history raw
1module Effect.State
3import Effects
5%access public
7data State : Effect where
8 Get : sig State a a
9 Put : b -> sig State () a b
11-- using (m : Type -> Type)
12instance 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 x [STATE x]
20get = call $ Get
22put : x -> Eff () [STATE x]
23put val = call $ Put val
25putM : y -> Eff () [STATE x] [STATE y]
26putM val = call $ Put val
28update : (x -> x) -> Eff () [STATE x]
29update f = put (f !get)
31updateM : (x -> y) -> Eff () [STATE x] [STATE y]
32updateM f = putM (f !get)
34locally : x -> (Eff t [STATE x]) -> Eff t [STATE y]
35locally newst prog = do st <- get
36 putM newst
37 val <- prog
38 putM st
39 return val