0 | module Control.Comonad.Store.Store
 1 |
 2 | import Control.Comonad
 3 | import Control.Comonad.Trans
 4 | import Control.Monad.Identity
 5 |
 6 | %default total
 7 |
 8 | public export
 9 | record StoreT (s : Type) (w : Type -> Type) (a : Type) where
10 |   constructor MkStoreT
11 |   run : w (s -> a)
12 |   val : s
13 |
14 | public export
15 | Store : (s : Type) -> (a : Type) -> Type
16 | Store s = StoreT s Identity
17 |
18 | ||| Create a Store using an accessor function and a stored value
19 | public export
20 | store : (s -> a) -> s -> Store s a
21 | store f s = MkStoreT (Id f) s
22 |
23 | public export
24 | runStore : Store s a -> (s -> a, s)
25 | runStore (MkStoreT (Id f) s) = (f, s)
26 |
27 | public export
28 | runStoreT : StoreT s w a -> (w (s -> a), s)
29 | runStoreT (MkStoreT wf s) = (wf, s)
30 |
31 | --------------------------------------------------------------------------------
32 | --          Interface Implementations
33 | --------------------------------------------------------------------------------
34 |
35 | public export
36 | Functor w => Functor (StoreT s w) where
37 |   map f = { run $= map (f .) }
38 |
39 | appEnv : (s -> a -> b) -> (s -> a) -> s -> b
40 | appEnv ff fa s = ff s (fa s)
41 |
42 | public export
43 | (Monoid s, Applicative w) => Applicative (StoreT s w) where
44 |   pure a = MkStoreT (pure $ const a) neutral
45 |   MkStoreT f m <*> MkStoreT a n = MkStoreT [| appEnv f a |]  (m <+> n)
46 |
47 | public export
48 | Comonad w => Comonad (StoreT s w) where
49 |   extract (MkStoreT wf s)   = extract wf s
50 |   duplicate (MkStoreT wf s) = MkStoreT (extend MkStoreT wf) s
51 |   extend f (MkStoreT wf s)  =
52 |     MkStoreT (extend (\wf',s' => f (MkStoreT wf' s')) wf) s
53 |
54 | public export
55 | ComonadTrans (StoreT s) where
56 |   lower (MkStoreT f s) = map ($ s) f
57 |
58 | public export
59 | (ComonadApply w, Semigroup s) => ComonadApply (StoreT s w) where
60 |   MkStoreT f m <@> MkStoreT a n = MkStoreT (map appEnv f <@> a) (m <+> n)
61 |