[Agda-dev] Using the size solver to get proto-cumulativity

[Jesper Cockx]

Hi Pelo,

Thanks for your mail! It's indeed an attractive idea in theory to merge
sizes and levels into a common type of ordinals. Unfortunately there are
currently still quite a few open issues related to sized types and size
subtyping in particular (see https://github.com/agda/agda/labels/sized-types),
so I would be reluctant to carry out such a merger at the moment. There are
also a few subtle differences between the typing rules for sizes and for
levels; for example the size solver instantiates unsolved sizes to
infinity, but this would make no sense for levels. Instead, for levels we
want to find the *smallest* consistent assignment.

During the last Agda meeting, I experimented with adding cumulativity to
Agda, but I got stuck on the problem that in the presence of subtyping, we
cannot trust the constraint solver to produce well-typed solutions. For
example, we may have a metavariable `_X : Set0` and a constraint `_X =?=
Set0 : Set1` (note that this constraint is well-typed since both `_X :
Set1` and `Set0 : Set1`). However, we should *not* instantiate `_X := Set`,
since we don't have `Set : Set`. So to properly implement subtyping we need
some way to 'downcast' metavariable solutions to their actual type. I
started experimenting with a solution to this problem using `checkInternal`
(see the --double-check flag on master for the current status), but a more
direct approach for downcasting could work as well.

Once this problem is solved, there is still the *real* problem, namely how
to find the smallest consistent solution for a system of level
metavariables and (in)equalities between them. Here your proposal of
reusing the size solver could work, but the solver would have to be
extended to deal with the `lub` constructor. This is especially hard if
`lub` can occur on the right side on an inequality, since there are two
possible solutions: if `a =< lub b c`, then either `a =< b` or `a =< c`,
but we don't know which one. To avoid this problem, we could maybe enforce
some style of using levels that prevents the creation of such constraints,
e.g. don't use `lub` in the return type of a function.

In Coq they have recently solved the problem of having cumulativity +
explicit universe polymorphism (see
https://www.irif.fr/~sozeau/research/publications/drafts/unification-jfp.pdf).
However, there are some caveats for adopting this approach in Agda:
- Coq doesn't care about uniqueness of metavariable solutions as much as
Agda, so a solver for Agda would have to be more conservative.
- In Coq, universe metavariables cannot depend on ordinary variables/terms
since levels cannot be computed from terms, but in Agda they can. This
makes it hard to implement a solver that deals *just* with levels without
worrying about arbitrary terms.
- The implementation of Coq's solver is quite complex, so it would take
nontrivial effort to implement the same thing for Agda.

All of this is certainly not meant to discourage you from looking into this
approach further, quite the opposite :) If you (or anyone else) are
interested in helping out, I would recommend to first look into the current
problems with subtyping we already have for sized types, since they will
only become worse once we add other kinds of subtyping such as cumulativity.

Cheers,
Jesper

ps: I'm very interested in working more on this stuff. If you want me to
elaborate more on some part of this mail, just ask!




On Tue, Jun 26, 2018 at 12:36 AM, peio borthelle <pborthelle at hadoly.fr>
wrote:

> Hi, new here! This is a follow-up from irc (i'm lapinot).
>
> So basically i wondered if it had already been investigated to give levels
> the same
> kind of interface as the current sizes (and if it has, what are the
> pitfalls). To
> explain a bit more what i mean, the crucial point is probably having a
> subtyping
> relationship but only for levels. I guess it would look like:
>
> postulate
>   LevelUniv : LevelUniv
>   Level : LevelUniv
>   Level<= : Level -> LevelUniv
>   lzero : Level
>   lsuc : Level -> Level
>   lub : Level -> Level -> Level
>
> Together with a subtyping relationships `if a <= b, Level<= a <: Level<=
> b`, `if a :
> Level, a : Level<= a` and `LevelUniv <: Set`. I guess that we could then
> create a
> type of explicitely cumulative sets:
>
> CSet : (a : Level) -> Set (lsuc a)
> CSet a = Sigma (Level<= a) (\ b -> Set b)
>
> Incidentally we could also get rid of the most annoying instances of
> `Lift`-hell that
> arise when trying to give smaller than intended sets as parameters to some
> structure.
>
> data Ugly (a : Level) : Set (lsuc a) where
>   con : Set a -> Foo
>
> -- throws in wrapping/unwrapping, clutters the output type (affects next
> definitions)
> ugly : {a b} -> Set a -> Ugly (a lub b)
> ugly X = con (Lift X)
>
> -- no wrapping, clean interface
> data Nice (a : Level) : Set (lsuc a) where
>   con : {b : Level<= a} -> Set b -> Foo
>
>
> Note that this whole thing may be actually hard if the generated
> constraints are hard
> to solve, but until now i failed to see how they could be different than
> the one for
> the sizes. There was some point about uniqueness of the solutions, i'm not
> sure how
> this is handled by the sizes (is size uniqueness required?). Yet it might
> be pretty
> reasonable to select the smallest solution.
>
> If this approach works, it may be interesting to unify sizes and levels to
> a more
> abstract ordinal (heck we might even add `lim : (a : Ord) -> (Ord< a ->
> Ord) ->
> Ord`!). I guess that nothing stops us from using the same type to index
> sets (which
> is already a core language type, thus magic) and to help solving
> termination.
>
> Cheers,
> peio
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda-dev/attachments/20180626/11c7ad0c/attachment.html>