Control.Monad.Free

Definitions

data Free : ((Type -> Type) -> Type -> Type) -> Type -> Type

  Higher-order free monad.
  Acts as a syntax generator of effectful programs.

Totality: not strictly positive
Visibility: public export
Constructors:

Return : a -> Free sig a

Op : sig (Free sig) a -> Free sig a

Hints:

Syntax sig => Applicative (Free sig)

Syntax sig => Functor (Free sig)

Syntax sig => Monad (Free sig)

return : a -> Free sig a

Visibility: public export

inject : Inj sub sup => sub (Free sup) a -> Free sup a

Visibility: public export

project : Prj sup sub => Free sup a -> Maybe (sub (Free sup) a)

Visibility: public export