Idris2Doc : Control.Monad.Free

Control.Monad.Free

(source)

Definitions

I : Type->Type
  The identity function specialized to `Type`.

Totality: total
Visibility: public export
0Arrs : (Type->Type) ->Type->Type->Type
  A type aligned sequence of bind operations
over `Free f`.

Totality: total
Visibility: public export
dataFree : (Type->Type) ->Type->Type
Totality: total
Visibility: public export
Constructor: 
MkFree : FreeViewft->Arrsfta->Freefa

Hints:
Applicative (Freef)
Functor (Freef)
HasIOm=>HasIO (Freem)
Monad (Freef)
MonadRec (Freef)
dataFreeView : (Type->Type) ->Type->Type
Totality: total
Visibility: public export
Constructors:
Pure : a->FreeViewfa
Bind : fb-> (b->Freefa) ->FreeViewfa
fromView : FreeViewfa->Freefa
  Converts a view to the corresponding free monad. O(1).

Totality: total
Visibility: export
toView : Freefa->FreeViewfa
  Converts a free monad to a view representing it.
Amortized O(1).

Totality: total
Visibility: export
lift : fa->Freefa
  Lift an arbitrary functor into a free monad.

Totality: total
Visibility: export
wrap : f (Freefa) ->Freefa
Totality: total
Visibility: export
substFree : (fx->Freegx) ->Freefa->Freega
Totality: total
Visibility: export
resume' : (fb-> (b->Freefa) ->r) -> (a->r) ->Freefa->r
  Unwraps a single layer of `f`, providing the continuation.
Amortized O(1).

Totality: total
Visibility: export
resume : Functorf=>Freefa->Either (f (Freefa)) a
  Unwraps a single layer of the functor `f`.
Amortized O(1).

Totality: total
Visibility: export
mapK : (mt->nt) ->Freema->Freena
  Apply a morphism to change a free monad's functor.

Totality: total
Visibility: export
foldMap : MonadRecm=> (fx->mx) ->Freefa->ma
  Run a computation described as a free monad in
a stack safe manner.

Totality: total
Visibility: export
run : FreeIa->a
  Run a pure computation in a stack-safe manner.

Totality: total
Visibility: export
runM : Functorm=>MonadRecn=> (m (Freema) ->n (Freema)) ->Freema->na
Totality: total
Visibility: export