Functor.map instance with `Alternative`

Stream: lean4

[Devon Tuma]

When a type has both a Monad instance and an Alternative instance it seems that Lean opts to derive the map operation from Alternative rather than Monad, which aren't equal in general (although they are for e.g. OptionT). Basic example:

example {m : Type u → Type v} [Monad m] [Alternative m] [LawfulMonad m]
    {α β : Type u} (mx : m α) (f : α → β) :
    f <$> mx = do let x ← mx; return f x :=
  -- fails iff Alternative is included above
  by rw [map_eq_bind_pure_comp, Function.comp_def]

This makes it hard to write generic lemmas about the behavior of failure if you want to define something like this:

class LawfulAlternative (m : Type u → Type v) [Alternative m] [Monad m] where
  failure_bind' {α β : Type u} (g : α → m β) : failure >>= g = failure

is there a way to tell Lean to opt for a different type-class path in the definition of these lemmas besides writing out @Functor.map m diff_inst α β f mx?

[Devon Tuma]

Sorry if this should be in the general channel instead

[Devon Tuma]

It seems like the easiest way to handle this would be to have a type-class for just the syntax that Alternative extends that just provides the failure definition:

class Failure (f : Type u → Type v) where
  failure : {α : Type u} → f α

export Failure (failure)

class Alternative' (f : Type u → Type v) extends Failure f, Applicative f where
  orElse : {α : Type u} → f α → (Unit → f α) → f α

however Alternative is defined in core Lean so I'm not sure how possible it is to change this. My current solution has been to instead define things in reverse:

class Failure (m : Type u → Type v) where
  fail {α : Type u} : m α

instance {m : Type u → Type v} [h : Alternative m] : Failure m where
  fail := h.failure

And to then write lemmas in terms of that so Lean can't "see" the extra Applicative instance from Alternative. However this means that there are both Failure.fail and failure floating around as definitions. Is there a better way I should handle this?

[Eric Wieser]

does class AlternativeMonad f extends Monad f, Alternative f work for you?

[Devon Tuma]

That does seem like a more elegant solution and solves my initial issue. Would this be something reasonable for me to PR to mathlib with instances for Option/OptionT m?

[Devon Tuma]

I'm also not sure which of these would be considered more idiomatic for enforcing laws on the type:

class AlternativeMonad₁ (m : Type u → Type v) extends Monad m, Alternative m

-- Extra typeclass for laws
class LawfulAlternative₁ (m : Type u → Type v) [AlternativeMonad₁ m] where
  failure_bind {α β : Type u} (g : α → m β) : failure >>= g = failure

-- Law included already
class AlternativeMonad₂ (m : Type u → Type v) extends Monad m, Alternative m where
  failure_bind {α β : Type u} (g : α → m β) : failure >>= g = failure

[Eric Wieser]

class LawfulAlternativeMonad (m : Type u → Type v) [AlternativeMonad m] where
  failure_bind {α β : Type u} (g : α → m β) : failure >>= g = failure

looks like the approach consistent with what we have elsewhere

[Eric Wieser]

Or perhaps

class LawfulAlternativeMonad (m : Type u → Type v) [AlternativeMonad m] extends LawfulMonad m where
  failure_bind {α β : Type u} (g : α → m β) : failure >>= g = failure

[Devon Tuma]

The second is then sufficient to prove related things about map and seq, which should hold in any real use case I think

[Aaron Liu]

docs#LawfulBEq, docs#LawfulFunctor, docs#LawfulApplicative, etc. all use a mixin typeclass that extends the previous lawful versions.

class AlternativeMonad (m : Type u → Type v) extends Monad m, Alternative m

-- Extra typeclass for laws
class LawfulAlternative (m : Type u → Type v) [AlternativeMonad m] extends LawfulMonad m where
  failure_bind {α β : Type u} (g : α → m β) : failure >>= g = failure
  orElse_failure {α : Type u} (a : m α) : (a <|> failure) = a
  failure_orElse {α : Type u} (b : m α) : (failure <|> b) = b
  -- etc.

[Devon Tuma]

Opened a PR #22349. I'm a bit unsure what should go in Mathlib.Control vs. Batteries.Control, seems that at least lemmas like OptionT.run_failureand OptionT.run_mapConst could go to batteries instead. I have a lot of other lemmas of that kind sitting around that I'd like to port somewhere.

[Devon Tuma]

@Quang Dao I guess you have at least moved the monad lifting laws to batteries. Were you planning to do that for most things like this?

[Kim Morrison]

Batteries seems better to me. I'm not sure that Mathlib cares about these things without further motivation. :-)

[Quang Dao]

It does seem that Devon's PR contains natural AlternativeMonad instances for Set, Finset, List, etc. So they interact with other parts of mathlib