[Agda] Level constraints

[Martin Escardo]

There is one more option, which I favour: Feferman's "typical 
ambiguity", with Harper's algorithm or similar.

The idea is that you just write "Set", perhaps many times in the same 
definition, and then Agda adds (different) indices as appropriate. This 
feels like working with type-in-type, but it is actually working with 
what we already have, with the difference that the universe levels are 
inferred rather than written down.

Moreover, it should be possible to be compatible with what we already 
have (perhaps writing e.g. Set_0 rather than Set if that's what you 
really mean). So, if you put levels i,j,k in your context and write 
Set_i, Set_{i \sqcup j}, etc. then it would work as it does now, but if 
you write Set in several places in the same definition, then it would 
invoke the typical ambiguity conventions and algorithm to fill in the 
missing indices and the missing indices. This should make things much 
easier, very much in the spirit of implicit arguments.

Let Agda do the laborious, but routine, work of figuring out and writing 
down (implicitly) the optimal levels, and in cases where you want to be 
in control, use the current system (perhaps improved by cumulativity as 
below).

Currently, definitions with levels tend to obscure the essential aspects 
of types with an excessive amount of clutter, which is formally 
necessary but also distracting.

M.

On 14/11/13 18:43, Nils Anders Danielsson wrote:
> On 2013-11-14 16:34, Christian Sattler wrote:
>> What do you think?
>
> There are many options (at least if we restrict the discussion to
> lifting):
>
> * The status quo.
>
> * Something like what you suggest.
>
> * Some kind of cumulativity.
>
> * Conor's lifting primitive (Crude but Effective Stratification,
>    http://sneezy.cs.nott.ac.uk/epilogue/?p=857.html).
>
> * Allowing the solver to produce non-unique solutions. (I believe that
>    Mattieu has implemented something like this for Coq.)
>
> * …
>
> I think it would be interesting to see a careful discussion of the pros
> and cons of these different designs.
>

-- 
Martin Escardo
http://www.cs.bham.ac.uk/~mhe