0 | module Control.Effect.State
 1 |
 2 | import Control.EffectAlgebra
 3 | import Control.HigherOrder
 4 |
 5 | import Control.Monad.State
 6 |
 7 | import public Control.Effect.Reader
 8 | import public Control.Effect.Writer
 9 |
10 | ||| State effect - the union of Reader and Writer effects.
11 | public export
12 | StateE : Type -> (Type -> Type) -> (Type -> Type)
13 | StateE s = ReaderE s :+: WriterE s
14 |
15 | public export
16 | Inj (StateE s) sig => Inj (ReaderE s) sig where
17 |   inj = inj {sub = StateE s, sup = sig} . Inl
18 |
19 | public export
20 | Inj (StateE s) sig => Inj (WriterE s) sig where
21 |   inj = inj {sub = StateE s, sup = sig} . Inr
22 |
23 | -- public export
24 | -- get : Algebra sig m => Inj (StateE s) sig => m s
25 | -- get = send {sig} {eff = StateE s} (Inl Ask)
26 |
27 | -- public export
28 | -- put : Algebra sig m => Inj (StateE s) sig => s -> m ()
29 | -- put x = send {sig} {eff = StateE s} (Inr (Tell x))
30 |
31 | namespace Algebra
32 |   public export
33 |   [State] Algebra sig m => Algebra (StateE s :+: sig) (StateT s m) where
34 |     alg ctxx hdl (Inl (Inl Ask)) =
35 |       ST $ \s => pure {f = m} (s, (s <$ ctxx))
36 |     alg ctxx hdl (Inl (Inr (Tell s))) =
37 |       ST $ \_ => pure {f = m} (s, ctxx)
38 |     alg ctxx hdl (Inr x) = ST $ \r => do
39 |      res <- alg
40 |        {f = Functor.Compose}
41 |        (r, ctxx) h x
42 |      pure res
43 |      where
44 |       h : Handler ((s,) . ctx) n m
45 |       h =
46 |          (~<~)
47 |           {ctx1 = (s,), ctx2 = ctx}
48 |           {l = n}
49 |           {m = StateT s m} {n = m} (uncurry runStateT) hdl
50 |
51 |   %hint public export
52 |   HintState : Algebra sig m => Algebra (StateE s :+: sig) (StateT s m)
53 |   HintState = State
54 |