[Agda] Level constraints

[Matthieu Sozeau]

Hi all,

On 15 nov. 2013, at 14:50, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2013-11-14 23:05, Martin Escardo wrote:
>> I thought I argued in the previous message that typical ambiguity,
>> considered as a layer on top of what we have, precisely addresses the
>> first three points. I have no idea about the last.
> 
> Harper and Pollack (1991) describe several algorithms. I assume that you
> are referring to the one in Section 6.2 (with both typical ambiguity and
> universe polymorphism). I seem to recall reading that one implementation
> of this algorithm was very slow, but unfortunately I don't remember
> where I read this. Is Matthieu's implementation of universe polymorphism
> in Coq based on this algorithm?

Yes, more or less. It shouldn’t be much slower than explicit universes 
as in Agda though, especially as the graph of constraints has an optimized
representation (actually, it could be improved still in Coq). In the implementation,
getting good performance seems to rely on hashconsing/optimal sharing mainly.
On universe intensive code (HoTT/coq, a groupoid model, a setoid model, or setting
the basic datatypes of Coq polymorphic and compiling the stdlib), it seems
reasonably efficient.

Otherwise, the main issue with the naive implementation is the proliferation 
of dummy variables in the <= relation, e.g. in Agda you’d use one universe l 
everywhere whereas in Coq you naturally generate fresh levels ln <= ln-1 <= … l 
all representing l due to cumulativity. My minimization heuristic (very similarly 
to Pierce and Turner’s greedy local type inference algorithm), collapses them 
back to a single level l. In most cases you get exactly what the user would have 
written. And you can always resort to explicit levels if you like.

So it’s 1-2-4 and for 3, well you have 2.
Cheers,
— Matthieu