Control.MonadRec

Reexports

Definitions

data Step : (a -> a -> Type) -> a -> Type -> Type -> Type

  Single step in a recursive computation.
  
  A `Step` is either `Done`, in which case we return the
  final result, or `Cont`, in which case we continue
  iterating. In case of a `Cont`, we get a new seed for
  the next iteration plus an updated state. In addition
  we proof that the sequence of seeds is related via `rel`.
  If `rel` is well-founded, the recursion will provably
  come to an end in a finite number of steps.

Totality: total
Visibility: public export
Constructors:

Cont : (seed2 : a) -> (0 _ : rel seed2 seed) -> st -> Step rel seed st res

  Keep iterating with a new `seed2`, which is
  related to the current `seed` via `rel`.
  `vst` is the accumulated state of the iteration.

Done : res -> Step rel v st res

  Stop iterating and return the given result.

Hint: 

Bifunctor (Step rel seed)

interface MonadRec : (Type -> Type) -> Type

  Interface for tail-call optimized monadic recursion.

Parameters: m
Constraints: Monad m
Methods:

tailRecM : (seed : a) -> (0 _ : Accessible rel seed) -> st -> ((seed2 : a) -> st -> m (Step rel seed2 st b)) -> m b

  Implementers must make sure they implement this function
  in a tail recursive manner.
  The general idea is to loop using the given `step` function
  until it returns a `Done`.
  
  To convey to the totality checker that the sequence
  of seeds generated during recursion must come to an
  end after a finite number of steps, this function
  requires an erased proof of accessibility.

Implementations:

MonadRec Identity

MonadRec Maybe

MonadRec (Either e)

MonadRec IO

MonadRec m => MonadRec (StateT s m)

MonadRec m => MonadRec (EitherT e m)

MonadRec m => MonadRec (MaybeT m)

MonadRec m => MonadRec (ReaderT e m)

MonadRec m => MonadRec (WriterT w m)

MonadRec m => MonadRec (RWST r w s m)

MonadRec Eval

tailRecM : MonadRec m => (seed : a) -> (0 _ : Accessible rel seed) -> st -> ((seed2 : a) -> st -> m (Step rel seed2 st b)) -> m b

  Implementers must make sure they implement this function
  in a tail recursive manner.
  The general idea is to loop using the given `step` function
  until it returns a `Done`.
  
  To convey to the totality checker that the sequence
  of seeds generated during recursion must come to an
  end after a finite number of steps, this function
  requires an erased proof of accessibility.

Totality: total
Visibility: public export

trWellFounded : MonadRec m => {auto 0 _ : WellFounded a rel} -> a -> st -> ((seed2 : a) -> st -> m (Step rel seed2 st b)) -> m b

  Monadic tail recursion over a well-founded structure.

Totality: total
Visibility: public export

trSized : MonadRec m => {auto 0 {conArg:3222} : Sized a} -> a -> st -> ((v : a) -> st -> m (Step Smaller v st b)) -> m b

  Monadic tail recursion over a sized structure.

Totality: total
Visibility: public export