0 | module Control.Effect.Labelled
 1 |
 2 | import Control.EffectAlgebra
 3 |
 4 | ||| Wrap an effect in a label.
 5 | ||| This can help disambiguate between multiple identical effects and
 6 | ||| lessen the number of type annotations.
 7 | public export
 8 | data Labelled : (label : k)
 9 |              -> (sub : (Type -> Type) -> (Type -> Type))
10 |              -> (m : Type -> Type) -> (Type -> Type) where
11 |   MkLabelled : (eff : sub m a) -> Labelled label sub m a
12 |
13 | public export
14 | runLabelled : Labelled label sub m a -> sub m a
15 | runLabelled (MkLabelled eff) = eff
16 |
17 | public export
18 | Functor (sub m) => Functor (Labelled label sub m) where
19 |   map f (MkLabelled x) = MkLabelled (map f x)
20 |
21 | public export
22 | Applicative (sub m) => Applicative (Labelled label sub m) where
23 |   pure x = MkLabelled (pure x)
24 |
25 |   (MkLabelled f) <*> (MkLabelled x) = MkLabelled (f <*> x)
26 |
27 | public export
28 | Monad (sub m) => Monad (Labelled label sub m) where
29 |   (MkLabelled x) >>= f = MkLabelled (x >>= runLabelled . f)
30 |
31 | public export
32 | Algebra (eff :+: sig) (sub m)
33 |   => Algebra (Labelled label eff :+: sig)
34 |              (Labelled label sub m) where
35 |   alg ctxx hdl (Inl (MkLabelled x)) = MkLabelled $
36 |     alg {sig = eff :+: sig, m = sub m}
37 |         ctxx (runLabelled . hdl) (Inl x)
38 |   alg ctxx hdl (Inr x) = MkLabelled $
39 |     alg {sig = eff :+: sig, m = sub m}
40 |         ctxx (runLabelled . hdl) (Inr x)
41 |
42 | ||| Higher-order injections where signatures are inferred from the label.
43 | public export
44 | interface InjL (0 label : k)
45 |                (0 sub : (Type -> Type) -> (Type -> Type))
46 |                (0 sup : (Type -> Type) -> (Type -> Type)) | label where
47 |   constructor MkSubL
48 |   injLabelled : Labelled label sub m a -> sup m a
49 |
50 | public export
51 | [LabelAuto] Inj sub sup => InjL label sub sup where
52 |   injLabelled (MkLabelled x) = inj x
53 |
54 | public export
55 | Label : Inj sub sup -> InjL label sub sup
56 | Label x = LabelAuto @{x}
57 |
58 | public export
59 | labelled : (label : k)
60 |         -> InjL label sub sig
61 |         => Algebra sig m
62 |         => sub m a -> m a
63 | labelled label @{sub} x =
64 |   let y = injLabelled (MkLabelled {label} x) in
65 |   alg {ctx = id} () id y
66 |