[Agda] How experimental is Cumulativity?

[Jon Sterling]

Indeed, very good points :)  I hope that someone will contribute a nice solver. Let me provide a few more remarks on cumulativity below which  may be of interest.

The version of type theory in which level coercions commute with type formers should be equivalent at the level of syntax (presentation) to the version where the coercions are omitted, so I expect this approach to be viable... (What I mean is, the subsumption rule can be viewed as a presentation of an actual / algebraically well-defined type theory which has sufficiently many equations on coercions.) For this reason, I take this style to be a _definition_ of cumulativity, considering that from an algebraic perspective, subtyping must be regarded as a notation and not as an objective construct.

But, I have found that even these "algebraically cumulative" hierarchies are likewise difficult to find in the wild, not much easier to model than the "materially" cumulative universes. The main advantage of the algebraic version of cumulativity is that it is well-defined mathematically (i.e. doesn't refer to raw terms), so it can be studied objectively.

For this reason, I am in the process of changing my tune and eating a bit of crow on my previous pronouncements; I increasingly think that those Lift types from Agda are good, but what we need a type theory in which they are built in, and in which the elaborator automatically inserts the appropriate coercions. With "Lift" types, there is an obvious "normal form" for the types of type theory, in which Lift is pushed to the leaves; the normalization I am referring to is 2-dimensional, in the sense that its trace exhibits an isomorphism between a type and its "normal form". I conjecture that these isomorphisms are coherent too, but I have not proved it.

I believe that this approach could be used in an elaborator, leading to a core type theory which is not so different from Agda's, but with a surface language which is significantly easier to use.

The main _noticeable_ difference between these weak hierarchies and the very strict algebraic-but-cumulative hierarchy in which coercions commute with connectives is to be detected when you form a dependent type _over_ the universe. Then, without some form of univalence, certain operations become impossible to define which had previously been definable in the context of the strict cumulativity. It remains to be seen whether this is a problem in practice.

Another relevant point is that taking cumulativity seriously should also involve a de-emphasis of the prevalent style of considering many universe level variables simultaneously. Cumulativity becomes unbelievably hard to deal with when you have many generic universe levels i,j,k... (requiring sophisticated solvers), but the ironic thing is that as soon as you have some form of cumulativity, it is sufficient to consider only _one_ generic universe level in practice.

Best wishes,
Jon


On Sat, Jan 4, 2020, at 11:23 AM, Jesper Cockx wrote:
> Hi Jon,
> 
> It's using material subtyping, so there's no coercions involved in the 
> resulting terms. You make a good point about the difficulty of finding 
> models, but I felt inserting actual coercions would be too hard to work 
> with in practical programming (essentially not much better than using 
> Lift in non-cumulative Agda). Perhaps a different approach where the 
> coercion from Set_i to Set_{i+k} commutes with other type formers would 
> be another viable solution if the current approach doesn't work.
> 
> You're correct that the interaction between material subtyping and 
> unification is quite tricky, currently Agda applies a few heuristics to 
> simplify equations between universe levels. If you are interested, you 
> can take a look at the functions `equalLevel` and `leqLevel` in 
> Conversion.hs 
> (https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/Conversion.hs#L1384 and https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/Conversion.hs#L1244) and `simplifyLevelConstraint` in LevelConstraints.hs (https://github.com/agda/agda/blob/dcb0f82f90fe44114d43303524a6fab5051bdaa2/src/full/Agda/TypeChecking/LevelConstraints.hs#L25). Really what we need is a good solver for level constraints. I think the problem is quite similar to the analogous one for sized types (which also is implemented using material subtyping), so my hope is that one solver could be general enough to handle both subsystems.
> 
> -- Jesper
> 
> 
> 
> On Sat, Jan 4, 2020 at 3:35 PM Jon Sterling <jon at jonmsterling.com> wrote:
> > Jesper,
> > 
> >  Is the cumulativity support based on "material subtyping" (I mean, elements of one universe really being elements of another universe) or is it based on elaboration of coercions?
> > 
> >  In the past I advocated this material subtyping, but these days I have been won over to coercions... mainly due to my suffering as I try to find models of type theory in places where it is no longer feasible to rely on the set-theoretic trickery which makes material cumulativity acceptable in, for instance, presheaf models a la Coquand.
> > 
> >  It also seems like the combination of material subtyping and unification may be a bit difficult to negotiate; I am curious how Agda's implementation deals with this, if it needs to.
> > 
> >  Best,
> >  Jon
> > 
> > 
> >  On Sat, Jan 4, 2020, at 9:07 AM, Jesper Cockx wrote:
> >  > Hi Joey,
> >  > 
> >  > The note that it is experimental mainly refers to the fact that there 
> >  > is no proper solver yet for level (in)equalities, so there will be 
> >  > (possibly quite frequent) cases where you have to fill in implicit 
> >  > level arguments that Agda is able to infer without --cumulativity. That 
> >  > being said, it is also a new feature in Agda and it hasn't been tested 
> >  > very extensively yet so there may also still be bugs of the "make Agda 
> >  > unsound" kind. Running Agda with the --double-check flag enabled might 
> >  > catch some of these bugs when they occur.
> >  > 
> >  > -- Jesper
> >  > 
> >  > ps: If anyone is interested in implementing a proper solver for 
> >  > universe levels, please get in touch! There may be some interesting 
> >  > research questions lurking there.
> >  > 
> >  > On Fri, Jan 3, 2020 at 8:28 PM Joey Eremondi <joey.eremondi at gmail.com> wrote:
> >  > > I see that Cumulativity is listed as an experimental feature in 2.6.1. Is this "the compiler might crash or reject valid programs" experimental? Or "Cumulativity might make Agda unsound" experimental? How much can I trust proofs that use cumulative Agda?
> >  > > 
> >  > > Thanks!
> >  > > _______________________________________________
> >  > > Agda mailing list
> >  > > Agda at lists.chalmers.se
> >  > > https://lists.chalmers.se/mailman/listinfo/agda
> >  > _______________________________________________
> >  > Agda mailing list
> >  > Agda at lists.chalmers.se
> >  > https://lists.chalmers.se/mailman/listinfo/agda
> >  >
> >  _______________________________________________
> >  Agda mailing list
> > Agda at lists.chalmers.se
> > https://lists.chalmers.se/mailman/listinfo/agda