Implementation Details #
Set of rewrite rules and automation for monads in general and
OptionT in particular.
The rewrite rules for monads are carefully chosen so that
simp with functor_norm will not introduce monadic vocabulary in a context where
applicatives would do just fine but will handle monadic notation
already present in an expression.
In a context where monadic reasoning is desired
simp with monad_norm
will translate functor and applicative notation into monad notation
and use regular
functor_norm rules as well.
functor, applicative, monad, simp
StateT program and discard the final state
- StateT.eval cmd s = Prod.fst <$> StateT.run cmd s
reduce the equivalence between two state monads to the equivalence between their respective function spaces
- StateT.equiv F = F
reduce the equivalence between two reader monads to the equivalence between their respective function spaces
- ReaderT.equiv F = F