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

[Eric Wieser]

Now that this has landed; is LawfulAlternative MetaM true, and should it be?

[Devon Tuma]

Thanks for getting the PR over the line on this. If we did have MetaM it would probably be this instance I guess

instance EStateM.alternativeMonad {ε σ} [Inhabited ε] :
    AlternativeMonad (EStateM ε σ) where
  failure := fun s => .error default s
  orElse x y := fun s => match x.run s with
    | .ok x s => .ok x s
    | .error _ s' => (y ()).run s' -- Don't revert state?

instance : AlternativeMonad Lean.Meta.MetaM := by
  refine @ReaderT.instAlternativeMonad _ _ ?_
  refine @StateRefT'.instAlternativeMonad _ _ _ ?_
  refine @ReaderT.instAlternativeMonad _ _ ?_
  refine @StateRefT'.instAlternativeMonad _ _ _ ?_
  refine @EStateM.alternativeMonad _ _ _

This does require choosing a canonical default error for failure in EStateM

[Eric Wieser]

I don't think that's so, MetaM doesn't inherit it's alternative instance

[Eric Wieser]

batteries#1405 has a zero-line implementation of the instance you have there, with where alone

[Devon Tuma]

I think it is actually not possible to make EStateM lawful anyways (and so not MetaM either I don't think). See attempt here. The main issue being that failure needs to pick a canonical error to return, but the laws will expect that the actual error thrown is the one propogating through orElse

[Devon Tuma]

I think we'd need a seperate LawfulErrorMonad type-class for these to allow the laws to distinguish different errors

[Devon Tuma]

Also I realized writing this that we should probably require AlternativeMonad for LawfulAlternative, to ensure the instance is synthesized isn't made on the spot

[Eric Wieser]

Just to check, you're aware that docs#Lean.Meta.instAlternativeMetaM already exists, with failure = throwError "failure"?

[Devon Tuma]

I think even if you use that, you still have the problem that for x <|> failure = x to hold, the error from LHS must propagate if x fails. But for failure <|> x = x to hold, the error from the RHS must propagate if x fails. I don't think it's possible to unify those cases in general unless I'm missing something.

[Devon Tuma]

I could be wrong but it feels like these laws don't work well when you can fail multiple different ways

[Devon Tuma]

Maybe x <|> failure = x shouldn't actually be in the type-class? In general you are throwing away the error from x, not preserving it

[Eric Wieser]

Relatedly, this inspired me to make batteries#1406, which suggests that StateT has a slightly surprising implementation of throw.

[Devon Tuma]

I guess it is maybe intended to interact better with the base monad this way?