0 | module Control.Monad.TransitionIndexed
 1 |
 2 | export
 3 | infixl 1 >>>=, =<<<, >>>
 4 |
 5 | %hide Prelude.pure
 6 |
 7 | ||| A TransitionIndexed pointed type defines purity but is not necessarily
 8 | ||| Applicative.
 9 | public export
10 | interface TransitionIndexedPointed z (0 m : (ty : Type) -> z -> (ty -> z) -> Type) | m where
11 |   pure : {0 a : Type} -> {0 f : a -> z} -> (x : a) -> m a (f x) f
12 |
13 | ||| A TransitionIndexed monad is like an indexed monad but the third
14 | ||| index is determined by a function that takes the first index as input.
15 | |||
16 | ||| One readily available example of a type that fits this interface is
17 | ||| a type representing stateful transitions and the values that fall
18 | ||| out of them.
19 | |||
20 | ||| For example, take the final Door example from "Type-Driven Development with Idris."
21 | |||
22 | |||    data DoorCmd : (ty : Type) ->
23 | |||                   DoorState ->
24 | |||                   (ty -> DoorState) ->
25 | |||                   Type
26 | public export
27 | interface TransitionIndexedMonad z (0 m : (ty : Type) -> z -> (ty -> z) -> Type) | m where
28 |   bind : {0 x : z} -> {0 f : a -> z} -> {0 g : b -> z} -> m a x f -> ((res : a) -> m b (f res) g) -> m b x g
29 |
30 | public export
31 | (>>>=) : TransitionIndexedMonad z m => m a x f -> ((res : a) -> m b (f res) g) -> m b x g
32 | (>>>=) = bind
33 |
34 | ||| Flipped version of `>>>=
35 | public export
36 | (=<<<) : TransitionIndexedMonad z m => {0 a : Type} -> {0 f : a -> z} -> ((res : a) -> m b (f res) g) -> m a x f -> m b x g
37 | (=<<<) = flip (>>>=)
38 |
39 | public export
40 | (>>>) : TransitionIndexedMonad z m => m () x f -> Lazy (m b (f ()) g) -> m b x g
41 | (>>>) y w = y >>>= \() => w
42 |
43 | ||| Conditionally execute an expression when the boolean is true.
44 | export
45 | when : TransitionIndexedPointed z m => Bool -> Lazy (m () (f ()) f) -> m () (f ()) f
46 | when True w  = w
47 | when False w = pure ()
48 |
49 | ||| Execute an expression unless the boolean is true.
50 | export
51 | unless : TransitionIndexedPointed z m => Bool -> Lazy (m () (f ()) f) -> m () (f ()) f
52 | unless = when . not
53 |
54 | ||| Map each element of a structure to a computation, evaluate those
55 | ||| computations and discard the results.
56 | public export
57 | traverse_ : (Foldable t, TransitionIndexedPointed z m, TransitionIndexedMonad z m) => (a -> m b x (const x)) -> t a -> m () x (const x)
58 | traverse_ f = foldr (\x,acc => (f x) >>>= (const acc)) (pure ())
59 |
60 | ||| Evaluate each computation in a structure and discard the results.
61 | public export
62 | sequence_ : (Foldable t, TransitionIndexedPointed z m, TransitionIndexedMonad z m) => t (m a x (const x)) -> m () x (const x)
63 | sequence_ = foldr (\x, acc => x >>>= (const acc)) (pure ())
64 |
65 | ||| Like `traverse_` but with the arguments flipped.
66 | public export
67 | for_ : (Foldable t, TransitionIndexedPointed z m, TransitionIndexedMonad z m) => t a -> (a -> m b x (const x)) -> m () x (const x)
68 | for_ = flip traverse_
69 |
70 |