RFC: Make `IO` universe polymorphic

eric-wieser commented 10 months ago

Proposal

Right now, we have IO : Type → Type. This RFC suggests we change to IO : Type u → Type u.

This RFC does not suggest:

Making all monads polymorphic within a chain of binds. This requires a massive redesign, and the tradeoffs are unclear.
Changing any of the "real" IO api to operate in any universe other than 0.

User Experience: How does this feature improve the user experience?
- Users of IO.ofExcept will not get weird universe errors if they pass in an Except from a higher universe
- Users of types in higher universes will not have to jump between the real IO monad and a hand-rolled IOButHigherUniverse
Beneficiaries: Which Lean users and projects benefit most from this feature/change?
- This would help with slim_check, which currently, in order to sample from types in higher universes, needs the monad itself to produce values in those universes
- Mathlib's existing ULiftable infrastructure would be usable with IO; currently it cannot be because IO doesn't form a family of types over universes.
- Users ask about this every few months
Maintainability: Will this change streamline code maintenance or simplify its structure?
- The change will replace a few (a b : Type u)s with (a : Type u) (b : Type v); the consequences are negligible.

Community Feedback

Some initial discussion, which suggests some benefit would arise even from just changing IO to allow higher universes: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/universe.20polymorphic.20IO/near/282494539

Impact

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

kim-em commented 10 months ago

I don't understand the motivation here. slim_check should not be sampling from higher universes in the first place.

kim-em commented 10 months ago

e.g.

import Std

example : ∃ (α : Type _) (l : List α), l ≠ l ++ l := by
  refine ⟨Int, ?_⟩
  refine ⟨[37], ?_⟩
  simp

eric-wieser commented 10 months ago

That example is a bit misleading, because Lean unifies the _ to 0. It fails if you use Type u.

eric-wieser commented 10 months ago

leanprover-community/mathlib4#9135 makes slim_check work on that statement, but it can't easily be generalized to do work in the IO monad unless we make the change suggested in this RFC.

Kha commented 3 weeks ago

How would you ever make use of a higher-universe IO if main etc. remain in IO.{0}?

eric-wieser commented 3 weeks ago

Making EStateM.bind universe-polymorphic, as I do in https://github.com/leanprover/lean4/pull/3010, is sufficient I think. You wouldn't be able to use do notation to jump between universes, but you could call EStateM.bind directly, or an IO.bind wrapper for it.

leanprover / lean4