Interesting thought. Transporting the concepts across naively, in Rust lifetime subtyping might correspond to cumulativity, and lifetime polymorphism to, well, universe polymorphism. But then what is shifting (and what is it useful for)?
Conversation
Btw, if you have any thoughts on this terminology bikeshed, please halp github.com/pikelet-lang/p
1
1
I seen it. I like "embiggening". Hope this helps! 😛
1
1
Arrgh I don't know what I was hoping for but thanks I think.
1
1
(I don't have nearly enough familiarity with / intuition for these matters to be able to give productive input alas)
1
Me niether. But you are a friend to cats, so I appreciate your input.
1
1
I just find the whole 'level' nomenclature annoying. WHY CAN'T IT BE 'SIZE'?
1
even the "size" nomenclature feels like a not-transparently-intuitive inheritance to me
(possibly they're called levels because it feels more natural to number them than sizes?)
1
broke: Type^0, Type^1, Type^2, Type^3...
woke: Type^XXS, Type^XS, Type^S, Type^M, Type^L, Type^XL...
1
1
Doll^0, Doll^1, Doll^2, ...
GIF
1
1
Would be super fun to use nesting doll metaphor on the universes page!