# Monad combinators, as in Haskell's Control.Monad. #

source
def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) :
m α

Collapses two layers of monadic structure into one, passing the effects of the inner monad through the outer.

Equations

- joinM a = a >>= id

Instances For

source
def condM {m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) :
m α

Executes `tm` or `fm` depending on whether the result of `mbool` is `true` or `false` respectively.

Equations

- condM mbool tm fm = do let b ← mbool bif b then tm else fm

Instances For