[Agda] How experimental is Cumulativity?

[Jesper Cockx]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200104/bb60bdcc/attachment.html>