[Agda] Level constraints

[Wolfram Kahl]

On Fri, Nov 15, 2013 at 09:32:45PM +0000, Martin Escardo wrote:
> 
> 
> On 15/11/13 19:02, Wolfram Kahl wrote:
> >Some of this can of course already be had by just writing ``Set _'',
> >as it occurs quite frequently in the standard library.
> >(I must admit that I do it rarely --- although I do have a definition
> >  that takes over 30 (implicit) Level parameters.)
> >
> >Making the underlying metavariable instantiation even more intelligent
> >would expand the opportunities for writing ``Set _''
> >without any change to the language ---
> >perhaps that could be one avenue for experimentation...
> 
> Nice, I will try to exploit this idea while typical ambiguity is not 
> available (I am sure we will manage to persuade the great and kind Agda 
> developers to eventually implement it). But I think the limitation of 
> your solution could be when it comes to situations where i \sqcup j is 
> needed for levels i and j, which is often the case

In the i <= j case implemented by i \sqcup j' that you mentioned previously,
you will need to make at least the key |Level|s explicit.
But in many cases, there is enough other material around that determines
the levels: In the standard library:

 $ grep ' → Set [^)}]*$' $(find . -name "*.agda") | wc -l
    211
 $ grep ' → Set [^)}]*$' $(find . -name "*.agda") | grep '_$' | wc
    115

Omit the `` | wc -l'' and you'll see what these look like...


> Are you suggesting to define something like
> 
> Type {i} = Set i
> 
> (if that's possible)

probably not possible...

> and then rely on implicit parameter inference to 
> simulate (some of) typical ambiguity?

Well, ``_'' is an explicit argument supplied implicitly,
just like ``{zero}'' in your ``Type ``{zero}'' would be
an implicit argument supplied explicitly.


Wolfram