Control.Monad.Pure

Reexports

Definitions

record Pure : Type -> Type -> Type

  A monad of pure computations with suport for localized
  mutable state.
  
  When universally quantified over `s`, this is like
  `Control.Monad.ST` from base, but proper compiler support
  for efficient code generation.
  
  On the other hand, `Pure World` is isomorphic to `IO`.

Totality: total
Visibility: public export
Constructor: 

P : F1 s a -> Pure s a

Projection: 

.run : Pure s a -> F1 s a

Hints:

Applicative (Pure s)

Applicative (Pure s)

Functor (Pure s)

Functor (Pure s)

HasIO (Pure World)

HasIO (Pure World)

Lift1 s (Pure s)

Lift1 s (Pure s)

Monad (Pure s)

Monad (Pure s)

.run : Pure s a -> F1 s a

Totality: total
Visibility: public export

run : Pure s a -> F1 s a

Totality: total
Visibility: public export

runPure : Pure s a -> a

  Runs a pure computation, probably with localized mutable state.

Totality: total
Visibility: export

runPureIO : HasIO io => Pure World a -> io a

  `Pure World` can be run in any monad that wraps `IO`.

Totality: total
Visibility: export