Commutative monads

def Monad.CommutativeAt (m : Type u → Type v) [Monad m] {α β : Type u} (ma : m α) (mb : m β) : Prop

Two monadic actions ma : m α and mb : m β are commutative if the following holds:

(do let a ← ma; let b ← mb; pure (a, b)) = (do let b ← mb; let a ← ma; pure (a, b))

class Monad.Commutative (m : Type u → Type v) [Monad m] : Prop

A monad is commutative if any two monadic actions ma : m α and mb : m β can be applied in any order. In other words, the following holds:

(do let a ← ma; let b ← mb; pure (a, b)) = (do let b ← mb; let a ← ma; pure (a, b))

• bind_comm {α β : Type u} (ma : m α) (mb : m β) : CommutativeAt m ma mb

@[simp]

theorem Monad.bind_comm_comp {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [Commutative m] {α β γ : Type u_1} (ma : m α) (mb : m β) (f : α × β → m γ) : (do let a ← ma let b ← mb f (a, b)) = do let b ← mb let a ← ma f (a, b)

theorem Monad.bind_swap {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [Commutative m] {α β γ : Type u_1} (ma : m α) (mb : m β) (f : α × β → m γ) : (do let a ← ma let b ← mb f (a, b)) = do let b ← mb let a ← ma f (a, b)

Alias of Monad.bind_comm_comp.

@[simp]

theorem Monad.CommutativeAt.bind_comm {m : Type (max u_1 u_2) → Type u_3} [Monad m] [LawfulMonad m] {α β : Type (max u_1 u_2)} (ma : m α) (mb : m β) (h : CommutativeAt m ma mb) : (do let a ← ma let b ← mb pure (a, b)) = do let b ← mb let a ← ma pure (a, b)

@[simp]

theorem Monad.CommutativeAt.bind_comm_comp {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] {α β γ : Type u_1} (ma : m α) (mb : m β) (h : CommutativeAt m ma mb) (f : α × β → m γ) : (do let a ← ma let b ← mb f (a, b)) = do let b ← mb let a ← ma f (a, b)

TODO: fix below lemmas & figure out a good naming scheme

theorem Monad.bind_comm_triple_swap_12 {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ : Type u_1} (ma : m α) (mb : m β) (mc : m γ) (f : α × β × γ → m δ) : (do let a ← ma let b ← mb let c ← mc f (a, b, c)) = do let b ← mb let a ← ma let c ← mc f (a, b, c)

Commutativity extends to sequences of three operations (swap first two)

theorem Monad.bind_comm_triple_swap_23 {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ : Type u_1} (ma : m α) (mb : m β) (mc : m γ) (f : α × β × γ → m δ) : (do let a ← ma let b ← mb let c ← mc f (a, b, c)) = do let a ← ma let c ← mc let b ← mb f (a, b, c)

Swap second and third elements in a triple of monadic actions

theorem Monad.bind_comm_quad_swap_12 {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ ε : Type u_1} (ma : m α) (mb : m β) (mc : m γ) (md : m δ) (f : α × β × γ × δ → m ε) : (do let a ← ma let b ← mb let c ← mc let d ← md f (a, b, c, d)) = do let b ← mb let a ← ma let c ← mc let d ← md f (a, b, c, d)

theorem Monad.bind_comm_quad_swap_23 {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ ε : Type u_1} (ma : m α) (mb : m β) (mc : m γ) (md : m δ) (f : α × β × γ × δ → m ε) : (do let a ← ma let b ← mb let c ← mc let d ← md f (a, b, c, d)) = do let a ← ma let c ← mc let b ← mb let d ← md f (a, b, c, d)

theorem Monad.bind_comm_quad_swap_34 {m : Type u_1 → Type u_2} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ ε : Type u_1} (ma : m α) (mb : m β) (mc : m γ) (md : m δ) (f : α × β × γ × δ → m ε) : (do let a ← ma let b ← mb let c ← mc let d ← md f (a, b, c, d)) = do let a ← ma let b ← mb let d ← md let c ← mc f (a, b, c, d)

instance Monad.instCommutativeId : Commutative Id

The identity monad is commutative

instance Monad.instCommutativeOption : Commutative Option

instance Monad.instCommutativeExceptOfSubsingleton {ε : Type u_1} [Subsingleton ε] : Commutative (Except ε)

instance Monad.instCommutativeReaderT {ρ : Type u_1} {m : Type u_1 → Type u_2} [Monad m] [Commutative m] : Commutative (ReaderT ρ m)

The ReaderT ρ m monad is commutative if the underlying monad is commutative

def Monad.Set.monadComm : Commutative Set

The set monad is commutative. This is not registered as an instance similar to how Set.monad is not registered as an instance.