RFC: generalize basic Inhabited/Nonempty instances from Monad to Applicative

Proposal

These instances are in Init.Prelude right after the definition of Monad:

instance {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) where
  default := pure

instance {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) where
  default := pure default

instance [Monad m] : [Nonempty α] → Nonempty (m α)
  | ⟨x⟩ => ⟨pure x⟩

I propose to generalize these instances to by moving them up a few lines after the definition of Applicative and modifying as follows:

instance {α : Type u} {f : Type u → Type v} [Applicative f] : Inhabited (α → f α) where
  default := pure

instance {α : Type u} {f : Type u → Type v} [Applicative f] [Inhabited α] : Inhabited (f α) where
  default := pure default

instance [Applicative f] : [Nonempty α] → Nonempty (f α)
  | ⟨x⟩ => ⟨pure x⟩

This change will facilitate writing partial definitions for applicative functors in the same way that the current definition allow writing partial definitions for monads.

The tentative PR #12041 suggests minimal side effects, maintenance costs are also expected to be minimal.

Community Feedback

The need for these instances has appeared in a recent Batteries PR (still under review). A discussion has been initiated on Zulip: #lean4 > Inhabited and Nonempty for Applicative

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start in Init.Prelude, where the three instances are currently defined after Monad, and compare the proposal with tentative PR #12041. Done means the instances are available after Applicative rather than requiring Monad, with minimal side effects as described in the issue.