0 | module Data.Union
 1 |
 2 | import Data.Subset
 3 |
 4 | %default total
 5 |
 6 | ||| A list of effect handlers handling effects of types `fs`
 7 | ||| wrapping results in type `m`.
 8 | public export
 9 | data Handler : (fs : List (Type -> Type)) -> (m : Type -> Type) -> Type where
10 |   Nil : Handler [] m
11 |   (::) : (h : forall x . f x -> m x) -> Handler fs m -> Handler (f :: fs) m
12 |
13 | ||| Sum type holding a value of type `t` wrapped in one of the
14 | ||| effect types listed in `fs`.
15 | public export
16 | data Union : (fs : List (Type -> Type)) -> (t : Type) -> Type where
17 |   U : (ix : Has f fs) -> (val : f t) -> Union fs t
18 |
19 | public export
20 | Uninhabited (Union [] t) where
21 |   uninhabited (U ix v) = absurd ix
22 |
23 | ||| Inject an effectful computation into a `Union`.
24 | public export %inline
25 | inj : (prf : Has f fs) => f t -> Union fs t
26 | inj = U prf
27 |
28 | ||| Tries to extract an effect from a `Union`.
29 | public export
30 | prj : (prf : Has f fs) => Union fs t -> Maybe (f t)
31 | prj {prf = Z}    (U Z v)     = Just v
32 | prj {prf = S ix} (U (S x) v) = prj {prf = ix} (U x v)
33 | prj _                        = Nothing
34 |
35 | ||| Extracts the last effect from a unary sum.
36 | public export
37 | prj1 : Union [f] t -> f t
38 | prj1 (U Z val) = val
39 | prj1 (U (S x) val) impossible
40 |
41 | ||| Handles all remaining effects via the given
42 | ||| (heterogeneous) list of event handlers.
43 | public export
44 | handleAll : Handler fs m -> Union fs t -> m t
45 | handleAll []       y              = absurd y
46 | handleAll (h :: t) (U Z val)     = h val
47 | handleAll (h :: t) (U (S y) val) = handleAll t (U y val)
48 |
49 | ||| Prepend a new effect to an existing `Union` value.
50 | public export
51 | weaken1 : Union fs a -> Union (f :: fs) a
52 | weaken1 (U ix val) = U (S ix) val
53 |
54 | public export
55 | weaken : Subset fs fs' => Union fs a -> Union fs' a
56 | weaken @{subset} (U ix val) = U (lemma_subset subset ix) val
57 |
58 |
59 | ||| Handle on of the effects in a `Union`. Unlike in other
60 | ||| effect libraries, it's not necessary that the effect
61 | ||| is the first in the list. To improve type inference,
62 | ||| the return type is calculated from the `prf` value.
63 | public export
64 | decomp :
65 |      {auto prf : Has f fs}
66 |   -> Union fs a
67 |   -> Either (Union (fs - f) a) (f a)
68 | decomp {prf = Z}                      (U Z     val) = Right $ val
69 | decomp {prf = Z}                      (U (S x) val) = Left $ U x val
70 | decomp {prf = S y} {fs = f :: h :: t} (U Z val)     = Left $ U Z val
71 | decomp {prf = S y} {fs = f :: h :: t} (U (S x) val) =
72 |   mapFst weaken1 $ decomp (U x val)
73 |
74 | ||| Handle one of the effects in a `Union`. Unlike in other
75 | ||| effect libraries, it's not necessary that the effect
76 | ||| is the first in the list. To improve type inference,
77 | ||| the return type is calculated from the `prf` value.
78 | public export
79 | handle :
80 |      {auto prf : Has f fs}
81 |   -> (f a -> res)
82 |   -> Union fs a
83 |   -> Either (Union (fs - f) a) res
84 | handle g = map g . decomp
85 |