-
Notifications
You must be signed in to change notification settings - Fork 415
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
RFC: Make IO
universe polymorphic
#3011
Comments
I don't understand the motivation here. |
e.g.
|
That example is a bit misleading, because Lean unifies the |
leanprover-community/mathlib4#9135 makes |
How would you ever make use of a higher-universe |
Making |
Proposal
Right now, we have
IO : Type → Type
. This RFC suggests we change toIO : Type u → Type u
.This RFC does not suggest:
User Experience: How does this feature improve the user experience?
IO.ofExcept
will not get weird universe errors if they pass in anExcept
from a higher universeIO
monad and a hand-rolledIOButHigherUniverse
Beneficiaries: Which Lean users and projects benefit most from this feature/change?
slim_check
, which currently, in order to sample from types in higher universes, needs the monad itself to produce values in those universesULiftable
infrastructure would be usable withIO
; currently it cannot be becauseIO
doesn't form a family of types over universes.Maintainability: Will this change streamline code maintenance or simplify its structure?
(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/282494539Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.
The text was updated successfully, but these errors were encountered: