def Control.Monad.join {α : Type} {m : Type → Type} [Monad m] (mma : m (m α)) : m α

Monadic join: flattens a nested monadic value.

$$\text{join} : m\,(m\;\alpha) \to m\;\alpha$$ $$\text{join}\;mma = mma \mathbin{>>=} \text{id}$$

Equations

• Control.Monad.join mma = mma >>= id

def Control.Monad.void {α : Type} {f : Type → Type} [Functor f] (fa : f α) : f Unit

Discard the result of a functor action, keeping only the effect.

$$\text{void} : f\;\alpha \to f\;\text{Unit}$$ $$\text{void}\;fa = (\lambda\;\_ \Rightarrow ()) \mathbin{<\$>} fa$$

Equations

• Control.Monad.void fa = (fun (x : α) => ()) <$> fa

def Control.Monad.when {m : Type → Type} [Monad m] (b : Bool) (action : m Unit) : m Unit

Conditional execution: run the action only when the boolean is true.

$$\text{«when»}\;b\;a = \begin{cases} a & \text{if } b \\ \text{pure}\;() & \text{otherwise} \end{cases}$$

Equations

• Control.Monad.when b action = if b = true then action else pure ()

def Control.Monad.unless {m : Type → Type} [Monad m] (b : Bool) (action : m Unit) : m Unit

Conditional execution: run the action only when the boolean is false.

$$\text{unless}\;b\;a = \text{when}\;(\lnot b)\;a$$

Equations

• Control.Monad.unless b action = Control.Monad.when (!b) action

def Control.Monad.mapM_ {α : Type u_1} {β : Type} {m : Type → Type} [Monad m] (f : α → m β) : List α → m Unit

Map a monadic function over a list, discarding the results.

$$\text{mapM\_}\;f\;[x_1, \ldots, x_n] = f\;x_1 \mathbin{>>} \cdots \mathbin{>>} f\;x_n \mathbin{>>} \text{pure}\;()$$

Equations

• Control.Monad.mapM_ f [] = pure ()
• Control.Monad.mapM_ f (x_1 :: xs) = do let _ ← f x_1 Control.Monad.mapM_ f xs

def Control.Monad.forM_ {α : Type u_1} {β : Type} {m : Type → Type} [Monad m] (xs : List α) (f : α → m β) : m Unit

Flipped mapM_: iterate over a list with a monadic action, discarding results.

$$\text{forM\_}\;xs\;f = \text{mapM\_}\;f\;xs$$

Equations

• Control.Monad.forM_ xs f = Control.Monad.mapM_ f xs

def Control.Monad.foldM {β : Type} {α : Type u_1} {m : Type → Type} [Monad m] (f : β → α → m β) (init : β) : List α → m β

Monadic left fold over a list.

$$\text{foldM}\;f\;z\;[x_1, \ldots, x_n] = f\;z\;x_1 \mathbin{>>=} \lambda z_1 \Rightarrow f\;z_1\;x_2 \mathbin{>>=} \cdots$$

Equations

• Control.Monad.foldM f init [] = pure init
• Control.Monad.foldM f init (x_1 :: xs) = do let acc ← f init x_1 Control.Monad.foldM f acc xs

def Control.Monad.filterM {α : Type} {m : Type → Type} [Monad m] (p : α → m Bool) : List α → m (List α)

Monadic filter: keep elements for which the predicate returns true in the monad.

$$\text{filterM}\;p\;xs = [x \in xs \mid p\;x]$$

Equations

• Control.Monad.filterM p [] = pure []
• Control.Monad.filterM p (x_1 :: xs) = do let b ← p x_1 let rest ← Control.Monad.filterM p xs pure (if b = true then x_1 :: rest else rest)

def Control.Monad.zipWithM {α : Type u_1} {β : Type u_2} {γ : Type} {m : Type → Type} [Monad m] (f : α → β → m γ) : List α → List β → m (List γ)

Monadic zip: apply a binary monadic function to corresponding elements.

$$\text{zipWithM}\;f\;[a_1, \ldots]\;[b_1, \ldots] = [f\;a_1\;b_1, f\;a_2\;b_2, \ldots]$$

Equations

• Control.Monad.zipWithM f [] x✝ = pure []
• Control.Monad.zipWithM f x✝ [] = pure []
• Control.Monad.zipWithM f (a :: as) (b :: bs) = do let c ← f a b let cs ← Control.Monad.zipWithM f as bs pure (c :: cs)

def Control.Monad.replicateM {α : Type} {m : Type → Type} [Monad m] (n : Nat) (ma : m α) : m (List α)

Repeat a monadic action n times, collecting the results.

$$\text{replicateM}\;n\;ma = [ma, ma, \ldots]\text{ (n times)}$$

Equations

• Control.Monad.replicateM 0 ma = pure []
• Control.Monad.replicateM n_2.succ ma = do let a ← ma let as ← Control.Monad.replicateM n_2 ma pure (a :: as)

def Control.Monad.replicateM_ {α : Type} {m : Type → Type} [Monad m] (n : Nat) (ma : m α) : m Unit

Repeat a monadic action n times, discarding the results.

$$\text{replicateM\_}\;n\;ma = ma \mathbin{>>} \cdots \mathbin{>>} ma \mathbin{>>} \text{pure}\;()$$

Equations

• Control.Monad.replicateM_ 0 ma = pure ()
• Control.Monad.replicateM_ n_2.succ ma = do let _ ← ma Control.Monad.replicateM_ n_2 ma

def Control.Monad.fish {α : Sort u_1} {β γ : Type} {m : Type → Type} [Monad m] (f : α → m β) (g : β → m γ) : α → m γ

Kleisli composition (left-to-right): $(f \mathbin{>=>} g)\;a = f\;a \mathbin{>>=} g$.

$$\text{fish} : (\alpha \to m\;\beta) \to (\beta \to m\;\gamma) \to \alpha \to m\;\gamma$$

Equations

• Control.Monad.fish f g a = f a >>= g

def Control.Monad.fishBack {β γ : Type} {α : Sort u_1} {m : Type → Type} [Monad m] (g : β → m γ) (f : α → m β) : α → m γ

Kleisli composition (right-to-left): $(g \mathbin{<=<} f) = f \mathbin{>=>} g$.

$$\text{fishBack} : (\beta \to m\;\gamma) \to (\alpha \to m\;\beta) \to \alpha \to m\;\gamma$$

Equations

• Control.Monad.fishBack g f = Control.Monad.fish f g

theorem Control.Monad.join_pure {α : Type} {m : Type → Type} [Monad m] [LawfulMonad m] (x : m α) : join (pure x) = x

Join-pure law: joining a pure value is the identity.

$$\text{join}\;(\text{pure}\;x) = x$$