0 | module Control.Comonad.Env.Env
 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 EnvT (e : Type) (w : Type -> Type) (a : Type)  where
10 |   constructor MkEnvT
11 |   env : e
12 |   val : w a
13 |
14 | public export
15 | Env : (e : Type) -> (a : Type) -> Type
16 | Env e = EnvT e Identity
17 |
18 | ||| Create an Env using an environment and a value
19 | public export
20 | mkEnv : e -> a -> Env e a
21 | mkEnv e a = MkEnvT e (Id a)
22 |
23 | public export
24 | runEnv : Env e a -> (e, a)
25 | runEnv (MkEnvT e (Id a)) = (e, a)
26 |
27 | public export
28 | runEnvT : EnvT e w a -> (e, w a)
29 | runEnvT (MkEnvT e wa) = (e, wa)
30 |
31 | ||| Modifies the environment using the specified function.
32 | public export
33 | local : (e -> e') -> EnvT e w a -> EnvT e' w a
34 | local f = { env $= f}
35 |
36 | --------------------------------------------------------------------------------
37 | --          Interface Implementations
38 | --------------------------------------------------------------------------------
39 |
40 | public export
41 | Functor w => Functor (EnvT e w) where
42 |   map g (MkEnvT e wa) = MkEnvT e (map g wa)
43 |
44 | public export
45 | (Monoid e, Applicative m) => Applicative (EnvT e m) where
46 |   pure = MkEnvT neutral . pure
47 |   MkEnvT ef wf <*> MkEnvT ea wa = MkEnvT (ef <+> ea) (wf <*> wa)
48 |
49 | public export
50 | Foldable w => Foldable (EnvT e w) where
51 |   foldl f acc = foldl f acc . val
52 |   foldr f acc = foldr f acc . val
53 |   null        = null . val
54 |
55 | public export
56 | Traversable w => Traversable (EnvT e w) where
57 |   traverse f (MkEnvT e w) = MkEnvT e <$> traverse f w
58 |
59 | public export
60 | Comonad w => Comonad (EnvT e w) where
61 |   duplicate (MkEnvT e wa) = MkEnvT e (extend (MkEnvT e) wa)
62 |   extract = extract . val
63 |
64 | public export
65 | ComonadTrans (EnvT e) where
66 |   lower (MkEnvT _ wa) = wa
67 |
68 | public export
69 | (Semigroup e, ComonadApply w) => ComonadApply (EnvT e w) where
70 |   MkEnvT ef wf <@> MkEnvT ea wa = MkEnvT (ef <+> ea) (wf <@> wa)
71 |