Laws for Monads with Failure

Definitions for monads that also have an Alternative instance while sharing the underlying Applicative instance, and a class LawfulAlternative for types where the failure and orElse operations behave in a natural way. More specifically they satisfy:

• f <$> failure = failure
• failure <*> x = failure
• x <|> failure = x
• failure <|> y = y
• x <|> y <|> z = (x <|> y) <|> z
• f <$> (x <|> y) = (f <$> x <|> f <$> y)

Option/OptionT are the most basic examples, but transformers like StateT also preserve the lawfulness of this on the underlying monad.

The law x *> failure = failure is true for monads like Option and List that don't have any "side effects" to execution, but not for something like OptionT on some monads, so we don't include this condition.

We also define a class LawfulAlternativeLift similar to LawfulMonadLift that states that a lifting between monads preserves failure and orElse.

Tags

monad, alternative, failure

class AlternativeMonad (m : Type u_1 → Type u_2) extends Alternative m, Monad m : Type (max (u_1 + 1) u_2)

AlternativeMonad m means that m has both a Monad and Alternative instance, which both share the same underlying Applicative instance. The main example is Option, but many monad transformers also preserve or add this structure.

• map {α β : Type u_1} : (α → β) → m α → m β
• mapConst {α β : Type u_1} : α → m β → m α
• pure {α : Type u_1} : α → m α
• seq {α β : Type u_1} : m (α → β) → (Unit → m α) → m β
• seqLeft {α β : Type u_1} : m α → (Unit → m β) → m α
• seqRight {α β : Type u_1} : m α → (Unit → m β) → m β
• failure {α : Type u_1} : m α
• orElse {α : Type u_1} : m α → (Unit → m α) → m α
• bind {α β : Type u_1} : m α → (α → m β) → m β

class LawfulAlternative (m : Type u_1 → Type u_2) [Alternative m] extends LawfulApplicative m : Prop

LawfulAlternative m means that the failure operation on m behaves naturally with respect to map, seq, and orElse operators.

• map_const {α β : Type u_1} : Functor.mapConst = Functor.map ∘ Function.const β
• id_map {α : Type u_1} (x : m α) : id <$> x = x
• comp_map {α β γ : Type u_1} (g : α → β) (h : β → γ) (x : m α) : (h ∘ g) <$> x = h <$> g <$> x
• seqLeft_eq {α β : Type u_1} (x : m α) (y : m β) : x <* y = Function.const β <$> x <*> y
• seqRight_eq {α β : Type u_1} (x : m α) (y : m β) : x *> y = Function.const α id <$> x <*> y
• pure_seq {α β : Type u_1} (g : α → β) (x : m α) : pure g <*> x = g <$> x
• map_pure {α β : Type u_1} (g : α → β) (x : α) : g <$> pure x = pure (g x)
• seq_pure {α β : Type u_1} (g : m (α → β)) (x : α) : g <*> pure x = (fun (h : α → β) => h x) <$> g
• seq_assoc {α β γ : Type u_1} (x : m α) (g : m (α → β)) (h : m (β → γ)) : h <*> (g <*> x) = Function.comp <$> h <*> g <*> x
• map_failure {α β : Type u_1} (f : α → β) : f <$> failure = failure

  Mapping the result of a failure is still a failure

• failure_seq {α β : Type u_1} (x : m α) : failure <*> x = failure

  Sequencing a failure call results in failure

• orElse_failure {α : Type u_1} (x : m α) : (x <|> failure) = x

  failure is a right identity for orElse.

• failure_orElse {α : Type u_1} (y : m α) : (failure <|> y) = y

  failure is a left identity for orElse.

• orElse_assoc {α : Type u_1} (x y z : m α) : (x <|> y <|> z) = ((x <|> y) <|> z)

  orElse is associative.

• map_orElse {α β : Type u_1} (x y : m α) (f : α → β) : f <$> (x <|> y) = (f <$> x <|> f <$> y)

  map commutes with orElse. The stronger statement with bind generally isn't true

@[simp]

theorem mapConst_failure {m : Type u_1 → Type u_2} {β α : Type u_1} [Alternative m] [LawfulAlternative m] (y : β) : Functor.mapConst y failure = failure

@[simp]

theorem mapConst_orElse {m : Type u_1 → Type u_2} {α β : Type u_1} [Alternative m] [LawfulAlternative m] (x x' : m α) (y : β) : Functor.mapConst y (x <|> x') = (Functor.mapConst y x <|> Functor.mapConst y x')

@[simp]

theorem failure_seqLeft {m : Type u_1 → Type u_2} {α β : Type u_1} [Alternative m] [LawfulAlternative m] (x : m α) : failure <* x = failure

@[simp]

theorem failure_seqRight {m : Type u_1 → Type u_2} {α β : Type u_1} [Alternative m] [LawfulAlternative m] (x : m α) : failure *> x = failure

@[simp]

theorem failure_bind {m : Type u_1 → Type u_2} {α β : Type u_1} [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m] (x : α → m β) : failure >>= x = failure

@[simp]

theorem seq_failure {m : Type u_1 → Type u_2} {α β : Type u_1} [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m] (x : m (α → β)) : x <*> failure = x *> failure

class LawfulAlternativeLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w) [Alternative m] [Alternative n] [MonadLift m n] : Prop

Type-class for monad lifts that preserve the Alternative operations.

• monadLift_failure {α : Type u} : monadLift failure = failure

  Lifting preserves failure.

• monadLift_orElse {α : Type u} (x y : m α) : monadLift (x <|> y) = (monadLift x <|> monadLift y)

  Lifting preserves orElse.

instance Option.instAlternativeMonad : AlternativeMonad Option

Equations

• Option.instAlternativeMonad = { toAlternative := instAlternativeOption, toBind := instMonadOption.toBind }

instance Option.instLawfulAlternative : LawfulAlternative Option

instance OptionT.instAlternativeMonadOfMonad (m : Type u_1 → Type u_2) [Monad m] : AlternativeMonad (OptionT m)

Equations

• OptionT.instAlternativeMonadOfMonad m = { toAlternative := OptionT.instAlternative, toBind := OptionT.instMonad.toBind }

instance OptionT.instLawfulAlternativeOfLawfulMonad (m : Type u_1 → Type u_2) [Monad m] [LawfulMonad m] : LawfulAlternative (OptionT m)

instance StateT.instAlternativeMonad {σ : Type u_1} (m : Type u_1 → Type u_2) [AlternativeMonad m] : AlternativeMonad (StateT σ m)

Equations

• StateT.instAlternativeMonad m = { toAlternative := StateT.instAlternative, toBind := StateT.instMonad.toBind }

instance StateT.instLawfulAlternativeOfLawfulMonad {σ : Type u_1} (m : Type u_1 → Type u_2) [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m] : LawfulAlternative (StateT σ m)

instance StateT.instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad {σ : Type u_1} (m : Type u_1 → Type u_2) [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m] : LawfulAlternativeLift m (StateT σ m)

instance ReaderT.instAlternativeMonad {m : Type u_1 → Type u_2} {ρ : Type u_1} [AlternativeMonad m] : AlternativeMonad (ReaderT ρ m)

Equations

• ReaderT.instAlternativeMonad = { toAlternative := ReaderT.instAlternativeOfMonad, toBind := ReaderT.instMonad.toBind }

instance ReaderT.instLawfulAlternative {m : Type u_1 → Type u_2} {ρ : Type u_1} [AlternativeMonad m] [LawfulAlternative m] : LawfulAlternative (ReaderT ρ m)

instance ReaderT.instLawfulAlternativeLift {m : Type u_1 → Type u_2} {ρ : Type u_1} [AlternativeMonad m] : LawfulAlternativeLift m (ReaderT ρ m)

instance StateRefT'.instAlternativeMonad {m : Type → Type} {ω σ : Type} [AlternativeMonad m] : AlternativeMonad (StateRefT' ω σ m)

Equations

• StateRefT'.instAlternativeMonad = { toAlternative := StateRefT'.instAlternativeOfMonad, toBind := StateRefT'.instMonad.toBind }

instance StateRefT'.instLawfulAlternative {m : Type → Type} {ω σ : Type} [AlternativeMonad m] [LawfulAlternative m] : LawfulAlternative (StateRefT' ω σ m)

instance StateRefT'.instLawfulAlternativeLift {m : Type → Type} {ω σ : Type} [AlternativeMonad m] : LawfulAlternativeLift m (StateRefT' ω σ m)