Control.Monad.TransitionIndexed

Definitions

interface TransitionIndexedPointed : (z : Type) -> ((ty : Type) -> z -> (ty -> z) -> Type) -> Type

  A TransitionIndexed pointed type defines purity but is not necessarily
  Applicative.

Parameters: z, m
Methods:

pure : (x : a) -> m a (f x) f

pure : TransitionIndexedPointed z m => (x : a) -> m a (f x) f

Visibility: public export

interface TransitionIndexedMonad : (z : Type) -> ((ty : Type) -> z -> (ty -> z) -> Type) -> Type

  A TransitionIndexed monad is like an indexed monad but the third
  index is determined by a function that takes the first index as input.
  
  One readily available example of a type that fits this interface is
  a type representing stateful transitions and the values that fall
  out of them.
  
  For example, take the final Door example from "Type-Driven Development with Idris."
  
     data DoorCmd : (ty : Type) ->
                    DoorState ->
                    (ty -> DoorState) ->
                    Type

Parameters: z, m
Methods:

bind : m a x f -> ((res : a) -> m b (f res) g) -> m b x g

bind : TransitionIndexedMonad z m => m a x f -> ((res : a) -> m b (f res) g) -> m b x g

Visibility: public export

(>>>=) : TransitionIndexedMonad z m => m a x f -> ((res : a) -> m b (f res) g) -> m b x g

Visibility: public export
Fixity Declarations:
infixl operator, level 1
infixl operator, level 1

(=<<<) : TransitionIndexedMonad z m => ((res : a) -> m b (f res) g) -> m a x f -> m b x g

  Flipped version of `>>>=

Visibility: public export
Fixity Declarations:
infixl operator, level 1
infixl operator, level 1

(>>>) : TransitionIndexedMonad z m => m () x f -> Lazy (m b (f ()) g) -> m b x g

Visibility: public export
Fixity Declarations:
infixl operator, level 1
infixl operator, level 1

when : TransitionIndexedPointed z m => Bool -> Lazy (m () (f ()) f) -> m () (f ()) f

  Conditionally execute an expression when the boolean is true.

Visibility: export

unless : TransitionIndexedPointed z m => Bool -> Lazy (m () (f ()) f) -> m () (f ()) f

  Execute an expression unless the boolean is true.

Visibility: export

traverse_ : (Foldable t, (TransitionIndexedPointed z m, TransitionIndexedMonad z m)) => (a -> m b x (const x)) -> t a -> m () x (const x)

  Map each element of a structure to a computation, evaluate those
  computations and discard the results.

Visibility: public export

sequence_ : (Foldable t, (TransitionIndexedPointed z m, TransitionIndexedMonad z m)) => t (m a x (const x)) -> m () x (const x)

  Evaluate each computation in a structure and discard the results.

Visibility: public export

for_ : (Foldable t, (TransitionIndexedPointed z m, TransitionIndexedMonad z m)) => t a -> (a -> m b x (const x)) -> m () x (const x)

  Like `traverse_` but with the arguments flipped.

Visibility: public export