0 | module Control.Effect.NonDet
 1 |
 2 | import Control.EffectAlgebra
 3 |
 4 | import Control.Monad.List
 5 |
 6 | import Data.List1
 7 |
 8 | ||| Add non-determinism to a computation,
 9 | ||| e.i. alternatives for program flow.
10 | ||| Choice between these alternatives is not directly specified and is
11 | ||| deferred to a particular handler.
12 | public export
13 | data ChoiceE : (Type -> Type) -> (Type -> Type) where
14 |   Choose : List (Inf (m a)) -> ChoiceE m a
15 |
16 | namespace Algebra
17 |   alg :   Algebra sig m
18 |        => (f : Functor ctx)
19 |        => ctx ()
20 |        -> Handler ctx n (ListT m)
21 |      -> (ChoiceE :+: sig) n a
22 |      -> (ListT m) (ctx a)
23 |   alg ctxx hdl (Inl (Choose list)) =
24 |     go list
25 |    where
26 |     go : List (Inf (n a)) -> ListT m (ctx a)
27 |     go [] = pure []
28 |     go (x :: xs) = (<+>) @{ListT} (hdl (x <$ ctxx)) (go xs)
29 |   alg ctxx hdl (Inr other) =
30 |     -- hdl : Handler ctx n (ListT m)
31 |     -- hdl' : Handler (List m) (ListT m) m
32 |     -- ? : Handler (List m . ctx) n m
33 |     EffectAlgebra.alg {f = Functor.Compose @{ListM}}
34 |         {ctx = ListM m . ctx}
35 |         {m} (ctxx :: pure [])
36 |         ((~<~) @{%search} @{Functor.ListM} { ctx1 = ListM m
37 |                , ctx2 = ctx
38 |                , l = n
39 |                , m = ListT m
40 |                , n = m} f hdl) other
41 |    where
42 |     f : Handler (ListM m) (ListT m) m
43 |     f = join @{Monad.ListT} . pure
44 |
45 |   ||| Handle choice by accumulating all alternatives in a list transformer.
46 |   %hint export
47 |   Concat : (al : Algebra sig m) => Algebra (ChoiceE :+: sig) (ListT m)
48 |   Concat = MkAlgebra @{Monad.ListT} Algebra.alg
49 |
50 | ||| Introduce non-deterministic branching to a computation.
51 | public export
52 | oneOf : Inj ChoiceE sig
53 |      => Algebra sig m
54 |      => List a
55 |      -> m a
56 | oneOf list =
57 |   send (Choose (map (delay . pure) list))
58 |
59 | ||| Introduce non-deterministic branching to a computation.
60 | public export
61 | oneOfM : Inj ChoiceE sig
62 |      => Algebra sig m
63 |      => List (Inf (m a))
64 |      -> m a
65 | oneOfM list =
66 |   send (Choose list)
67 |