Experiment with Andras Korvacs' version of universe lifting about pikelet HOT 5 OPEN

Yes.

from pikelet.

I've read the report and Conor's post more carefully. In my previous comments I thought that my lifting is the same, but it's not. My implementation was about elaborating cumulative surface syntax to non-cumulative core. The other kind of lifting is an alternative to universe polymorphism. The two operations are very different, and they actually seem to be orthogonal. In principle, one could use my lifting (which is roughly the same as the lifting in Jon's paper) to emulate cumulativity, and the other lifting to emulate (some part of) universe polymorphism. The complications in Rouhling's report seem clearly necessary to me, and I also get now how lifting closed definitions is simpler.

Currently I'm more in favor of just biting the bullet and going full Coq: core syntax with implicit cumulative subtyping + universe polymorphism + constraint solving. It's not simple, but:

• Non-cumulativity as in Agda is annoying, and elaborating cumulativity to lifts (as in my demo) adds significant cost and noise.
• As soon as we want cumulativity (whether "emulated" or not) together with general-purpose unification, we need constraint solving for level ordering anyway! If I can write a hole in the program, in inference mode I need a level meta for the type of the hole. But note that level solving does not have to be very sophisticated to be useful.

So I think Conor-style lifting is probably a good design point if we don't have unification; otherwise it makes sense to extend existing machinery to deal with universe polymorphism.

from pikelet.

One potential downside of univ-lifts is that it seems to duplicate the evaluator to improve the elaboration output. See delift. Still trying to get my head around it, but perhaps the Internship Report's approach gets around this somehow? 🤔

from pikelet.

Thanks for the clarification! Sorry if I was confused too!

from pikelet.

Jon's paper

Oh I think I actually missed this one, which is also why I've been confused. Was that "Algebraic Type Theory and Universe Hierarchies"?

from pikelet.