Zulip Chat Archive
Stream: general
Topic: universe polymorphic version of empty?
Zesen Qian (Jul 05 2018 at 19:13):
RT? The current empty is at Type 0
Zesen Qian (Jul 05 2018 at 19:13):
just don't want to reinvent the wheel.
Also wondering why empty is not universe polymorphic
Chris Hughes (Jul 05 2018 at 19:16):
What situation would it be an advantage for empty to be polymorphic?
Zesen Qian (Jul 05 2018 at 19:17):
oh wait, is lean's universe cumulative?
Simon Hudon (Jul 05 2018 at 19:17):
If you need empty in universe u, you can use ulift.up.{u} empty. ulift is a tool to fit objects of different universes together.
Simon Hudon (Jul 05 2018 at 19:17):
No, it's not
Zesen Qian (Jul 05 2018 at 19:17):
very nice, thank you.
Simon Hudon (Jul 05 2018 at 19:18):
we use ulift when we would need cumulativeness
Simon Hudon (Jul 05 2018 at 19:20):
In general, you should use universe variables as rarely as possible and use ulift. When you build definitions like list, you have no choice to make it universe polymorphic so that it can be used in various universes: list : Type u -> Type u. That's because if list : Type -> Type, there's no way of using lift on a : Type 3 in order to have a list a
Zesen Qian (Jul 05 2018 at 19:31):
ahh, can't understand the error
ulift Type
not match
Type u
Simon Hudon (Jul 05 2018 at 19:32):
Can you show the code?
Zesen Qian (Jul 05 2018 at 19:32):
def clause : list (Type u) → Type u
| ([]) := ulift.up.{u+1} empty
| (x :: xs) := sum x $ clause xs
Simon Hudon (Jul 05 2018 at 19:37):
Use ulift empty instead of ulift.up empty. ulift.up is something you use on a term. On a type, you use simply ulift
Last updated: Dec 20 2023 at 11:08 UTC