[Agda-dev] Implementing a solver for universe levels

[Jesper Cockx]

Hi Marko,

It's great to hear that you want to contribute to the implementation of
Agda!

Universe polymorphism is a relatively stable feature of Agda, though there
have been some recent changes due to issues found by the new internal
double-checker. OTOH Cumulativity is really new and hasn't got much testing
yet, so depending on its reception in the release it might stay relatively
unchanged or it might be removed/replaced entirely.

The current implementation of cumulativity makes use of a simple heuristic
to instantiate unsolved levels (at
https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/Level/Solve.hs):
if checking a signature or a definition produced unsolved level metas and
they are no lower bounds on those metas, instantiate them to the lowest
possible solution `lzero`. If you turn off this heuristic (e.g. by
commenting the line `defaultLevelsToZero newMetas` and recompiling Agda),
you can see some examples of the kind of constraints a solver would need to
handle. For example, on the file `test/Succeed/Cumulativity.agda`, I get
the following:

```
Failed to solve the following constraints:
  piSort (Set ℓ)
  (λ x →
     Set
     (ℓ ⊔ ℓ′ ⊔ _ℓ_247 (n = n) (P = P) (x = x) ⊔
      _ℓ′_248 (n = n) (P = P) (x = x)))
    =< Set (ℓ ⊔ ℓ′)
  ℓ ⊔ _ℓ₁_239 (n = (suc n)) = ℓ ⊔ _ℓ₁_239 (n = n) ⊔ _ℓ_247
  lsuc ℓ′ ⊔ _ℓ₂_240 (n = (suc n))
    = lsuc ℓ′ ⊔ _ℓ₂_240 (n = n) ⊔ lsuc _ℓ′_248
  A.ℓ ⊔ _ℓ_218 = A.ℓ ⊔ _ℓ_218 ⊔ _A.ℓ_226
  A.ℓ ⊔ _ℓ₁_216 = A.ℓ ⊔ _ℓ₁_216 ⊔ _A.ℓ_226
  B.ℓ ⊔ _ℓ₂_217 = B.ℓ ⊔ _ℓ₂_217 ⊔ _B.ℓ_227
  B.ℓ ⊔ _ℓ₂_191 ⊔ _B.ℓ_199 = B.ℓ ⊔ _ℓ₂_191
  A.ℓ ⊔ _ℓ₁_190 ⊔ _A.ℓ_198 = A.ℓ ⊔ _ℓ₁_190
  A.ℓ ⊔ _ℓ_189 ⊔ _A.ℓ_198 = A.ℓ ⊔ _ℓ_189
  lsuc (lsuc lzero) ⊔ _ℓ_120 (f = f)
    = lsuc (lsuc lzero) ⊔ _ℓ_74 (f = f) ⊔ _A.ℓ_127
  lsuc lzero ⊔ _ℓ_108 (f = f) = lsuc lzero ⊔ _ℓ_74 (f = f) ⊔ _A.ℓ_115
  lsuc lzero ⊔ _ℓ_75 (f = f) ⊔ _B.ℓ_103 = lsuc lzero ⊔ _ℓ_98 (f = f)
  A.ℓ ⊔ _ℓ_74 (f = f) = A.ℓ ⊔ _ℓ_74 (f = f) ⊔ _A.ℓ_80
  B.ℓ ⊔ _ℓ_75 (f = f) ⊔ _B.ℓ_81 = B.ℓ ⊔ _ℓ_75 (f = f)
  _ℓ_52 (ℓ′ = (lsuc (lsuc (lsuc lzero)))) ⊔ _ℓ_58 = lsuc lzero
  _ℓ_58 =< lsuc (lsuc (lsuc lzero))
  _ℓ_55 =< ℓ₁ ⊔ ℓ
  ℓ₁ ⊔ _ℓ_52 (ℓ′ = ℓ) ⊔ _ℓ_55 = ℓ₁ ⊔ _ℓ_52 (ℓ′ = ℓ)
```

I don't have a very clear idea yet how big of an effort the level solver
would be, but I expect it could be quite considerable. It will also depend
a lot on how powerful we want the solver to be. One point of reference is
the current size solver at
https://github.com/agda/agda/blob/master/src/full/Agda/TypeChecking/SizedTypes,
which is about 2000 lines (about half for the actual solver in
WarshallSolver.hs and half the interface with the rest of Agda in
Solver.hs). I would expect a solver for universe levels to be of a similar
size. Ideally, both levels and sizes would make use of the *same* solver
and only the interface with Agda would be different.

Since you're a new contributor to Agda, my recommendation would be to start
on something smaller to get a feeling for the Agda codebase. If you want to
do this, here are some issues related to universe levels that currently
need help: https://github.com/agda/agda/issues/4345,
https://github.com/agda/agda/issues/4119,
https://github.com/agda/agda/issues/3143. If you're keen to work on the
solver and understand that it might be a lot of work, a good point to start
would be to construct a few test cases that produce level constraints
currently not solved by Agda. Two such test cases (that don't even use
--cumulativity) are https://github.com/agda/agda/issues/3098 and
https://github.com/agda/agda/issues/2246.

I'm very glad to answer any questions you have while working on Agda!

-- Jesper



On Sun, Jan 5, 2020 at 11:53 PM Marko Dimjašević <marko at dimjasevic.net>
wrote:

> Dear Agda developers,
>
> The upcoming Agda 2.6.1 release features universe cumulativity [1]. In
> an email to the Agda users mailing list (agda at lists.chalmers.se),
> Jesper Cockx said the following about cumulativity [2]: "If anyone is
> interested in implementing a proper solver for universe levels, please
> get in touch!"
>
> I am interested to work on this!
>
> Would anyone be so kind to say a bit more about the problem, the
> current state of universe levels and of the cumulativity feature, which
> is marked experimental? Furthermore, how big an effort to implement a
> solver is considered to be?
>
> So far I made no coding contributions to Agda, though I've been a
> Haskell developer.
>
>
> [1] https://github.com/agda/agda/blob/release-2.6.1/CHANGELOG.md
> [2] https://lists.chalmers.se/pipermail/agda/2020/011486.html
>
>
> --
> Regards,
> Marko Dimjašević <marko at dimjasevic.net>
> https://dimjasevic.net/marko
> PGP key ID:       056E61A6F3B6C9323049DBF9565EE9641503F0AA
> Learn email self-defense! https://emailselfdefense.fsf.org
>
> _______________________________________________
> 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/20200106/0efc59d0/attachment.html>