
  0 | module Control.Applicative.Indexed
  1 | 
  2 | import Control.Functor.Indexed
  3 | 
  4 | export
  5 | infixl 3 <<*>>, <<*, *>>
  6 | 
  7 | public export
  8 | interface IndexedFunctor z z f => IndexedApplicative z f | f where
  9 |   total
 10 |   pure : {0 i : z} -> (x : a) -> f a i i
 11 | 
 12 |   total
 13 |   ap : {0 i,j,k : z} -> f (a -> b) i j -> f a j k -> f b i k
 14 | 
 15 | public export
 16 | (<<*>>) : IndexedApplicative z f => f (a -> b) i j -> f a j k -> f b i k
 17 | (<<*>>) = ap
 18 | 
 19 | public export
 20 | (<<*) : IndexedApplicative z f => f a i j -> f b j k -> f a i k
 21 | x <<* y = map const x <<*>> y
 22 | 
 23 | public export
 24 | (*>>) : IndexedApplicative z f => f a i j -> f b j k -> f b i k
 25 | x *>> y = map (const id) x <<*>> y
 26 | 
 27 | ||| Conditionally execute an applicative expression when the boolean is true.
 28 | public export
 29 | when : IndexedApplicative z f => Bool -> Lazy (f () i i) -> f () i i
 30 | when True y  = y
 31 | when False y = pure ()
 32 | 
 33 | ||| Execute an applicative expression unless the boolean is true.
 34 | %inline
 35 | public export
 36 | unless : IndexedApplicative z f => Bool -> Lazy (f () i i) -> f () i i
 37 | unless = when . not
 38 | 
 39 | ||| Map each element of a structure to a computation, evaluate those
 40 | ||| computations and discard the results.
 41 | public export
 42 | traverse_ : (Foldable t, IndexedApplicative z f) => (a -> f b i i) -> t a -> f () i i
 43 | traverse_ f = foldr ((*>>) . f) (pure ())
 44 | 
 45 | ||| Evaluate each computation in a structure and discard the results.
 46 | public export
 47 | sequence_ : (Foldable t, IndexedApplicative z f) => t (f a i i) -> f () i i
 48 | sequence_ = foldr (*>>) (pure ())
 49 | 
 50 | ||| Like `traverse_` but with the arguments flipped.
 51 | public export
 52 | for_ : (Foldable t, IndexedApplicative z f) => t a -> (a -> f b i i) -> f () i i
 53 | for_ = flip traverse_
 54 | 
 55 |