Experiment with Andras Korvacs' version of universe lifting

[brendanzab]

Currently we implement universe lifting based on "Dependently typed lambda calculus with a lifting operator (Internship Report)", which was inspired by Conor McBride's blog post, "Crude but Effective Stratification". Thanks goes to Jon Sterling for pointing us to this stuff! Unfortunately this version of McBride's idea is a bit fiddly, threading the accumulated universe offset through the evaluation environment. It also doesn't use coercions as a way to implement cumulativity, requiring us to have subtyping in the core language. From memory Jon Sterling avoided the complexity of the internship report in RedTT by restricting lifting to top level definitions, but this is not as useful in Pikelet where I'm trying to avoid top level definitions as much as possible.

@AndrasKovacs recently did an interesting lecture on universe lifting, Generalized universe hierarchies, which looks promising! There is a formalisation in Agda and a prototype implementation in Haskell using normalization-by-evaluation and coercive subtyping. I'm still trying to figure out what Up and Down do (these look like quote/unquote?), but it seems like the threading of the universe offsets through evaluation is avoided.

• AndrasKovacs/universes: formalisation in Agda
• AndrasKovacs/elaboration-zoo/.../univ-lifts: Universes indexed with natural numbers, with a lifting operation.

[brendanzab]

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? 🤔

[AndrasKovacs]

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.

[brendanzab]

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

[brendanzab]

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"?

[AndrasKovacs]

Yes.