# 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

source
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 β

Instances

source
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

Instances

source
@[simp]
theorem mapConst_failure {m : Type u_1 → Type u_2} {β α : Type u_1} [Alternative m] [LawfulAlternative m] (y : β) :
Functor.mapConst y failure = failure
source
@[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')
source
@[simp]
theorem failure_seqLeft {m : Type u_1 → Type u_2} {α β : Type u_1} [Alternative m] [LawfulAlternative m] (x : m α) :
failure <* x = failure
source
@[simp]
theorem failure_seqRight {m : Type u_1 → Type u_2} {α β : Type u_1} [Alternative m] [LawfulAlternative m] (x : m α) :
failure *> x = failure
source
@[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
source
@[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
source
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`.

Instances

source
instance Option.instAlternativeMonad :
AlternativeMonad Option
Equations

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

source
instance Option.instLawfulAlternative :
LawfulAlternative Option
source
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 }

source
instance OptionT.instLawfulAlternativeOfLawfulMonad (m : Type u_1 → Type u_2) [Monad m] [LawfulMonad m] :
LawfulAlternative (OptionT m)
source
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 }

source
instance StateT.instLawfulAlternativeOfLawfulMonad {σ : Type u_1} (m : Type u_1 → Type u_2) [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m] :
LawfulAlternative (StateT σ m)
source
instance StateT.instLawfulAlternativeLiftOfLawfulAlternativeOfLawfulMonad {σ : Type u_1} (m : Type u_1 → Type u_2) [AlternativeMonad m] [LawfulAlternative m] [LawfulMonad m] :
LawfulAlternativeLift m (StateT σ m)
source
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 }

source
instance ReaderT.instLawfulAlternative {m : Type u_1 → Type u_2} {ρ : Type u_1} [AlternativeMonad m] [LawfulAlternative m] :
LawfulAlternative (ReaderT ρ m)
source
instance ReaderT.instLawfulAlternativeLift {m : Type u_1 → Type u_2} {ρ : Type u_1} [AlternativeMonad m] :
LawfulAlternativeLift m (ReaderT ρ m)
source
instance StateRefT'.instAlternativeMonad {m : Type → Type} {ω σ : Type} [AlternativeMonad m] :
AlternativeMonad (StateRefT' ω σ m)
Equations

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

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