
  0 | module Control.Monad.Indexed
  1 | 
  2 | import Control.Functor.Indexed
  3 | import Control.Applicative.Indexed
  4 | 
  5 | export
  6 | infixl 1 >>>=, =<<<, >>>, >>=>, <=<<
  7 | 
  8 | public export
  9 | interface IndexedApplicative z m => IndexedMonad z m | m where
 10 |   total
 11 |   bind : {0 i,j,k : z} -> m a i j -> (a -> m b j k) -> m b i k
 12 | 
 13 |   total
 14 |   join : {0 i,j,k : z} -> m (m a j k) i j -> m a i k
 15 | 
 16 |   -- default implementations
 17 |   bind x f = join (map f x)
 18 |   join x = bind x id
 19 | 
 20 | public export
 21 | (>>>=) : IndexedMonad z m => m a i j -> (a -> m b j k) -> m b i k
 22 | (>>>=) = bind
 23 | 
 24 | ||| Flipped version of `>>>=`
 25 | public export
 26 | (=<<<) : IndexedMonad z m => (a -> m b j k) -> m a i j -> m b i k
 27 | (=<<<) = flip (>>>=)
 28 | 
 29 | ||| Sequence effects taking the value of the second.
 30 | public export
 31 | (>>>) : IndexedMonad z m => m () i j -> Lazy (m b j k) -> m b i k
 32 | (>>>) x y = x >>>= \_ => y
 33 | 
 34 | ||| Left-to-right Kleisli composition of indexed monads.
 35 | public export
 36 | (>>=>) : IndexedMonad z m => (a -> m b i j) -> (b -> m c j k) -> (a -> m c i k)
 37 | (>>=>) f g x = f x >>>= g
 38 | 
 39 | ||| Right-to-left Kleisli composition of indexed monads, flipped version of `>=>`.
 40 | public export
 41 | (<=<<) : IndexedMonad z m => (b -> m c j k) -> (a -> m b i j) -> (a -> m c i k)
 42 | (<=<<) = flip (>>=>)
 43 |