[Agda] More universe polymorphism

[Martin Escardo]

Hi Dan,

For example, I would like Agda to be just as it is currently with 
universe levels (not type:type, in particular), but, additionally, allow 
me to rely on "typical ambiguity" as a short-hand for boiler-plate 
schematic definitions.

"Set" should not be a short-hand for "Set lzero", but rather for "Set i" 
for a suitable level i (which Agda should figure out).

For example, if I write

funext : Set
funext = (X : Set) (Y : X -> Set) (f g : (x : X) -> Y x)
        -> ((x : X) -> f x == g x) -> f == g,

then I would expect Agda to figure out that I actually meant

funext : {i j : Level} -> Set(lsucc(lmax i j))
funext {i} {j} = (X : Set i ) (Y : X -> Set j) (f g : (x : X) -> Y x)
        -> ((x : X) -> f x == g x) -> f == g

At the moment I just write, in practice, e.g.

funext : Set1
funext = (X : Set0) (Y : X -> Set0) (f g : (x : X) -> Y x)
        -> ((x : X) -> f x == g x) -> f == g

because universe levels clutter types to the extent that their essence 
gets hidden.

And, at the moment, I don't need "Level" to be a type, and I would be 
happy to imagine that for each pair i,j (in my meta-language) I have a 
different definition funext{i}{j} (i.e. I am happy to work with 
schematic definitions which stand for countably many definitions (of 
which only finitely many can be used in each Agda program)).

When I call funext, I expect Agda to figure out which concrete pair i,j 
I meant, and tell me off if there isn't anything I could have sensibly 
meant.

The future may prompt me to want something more general like Guillaume 
Brunerie proposed, but for the present the above seems more than enough 
to me.

Moreover, yes, I would like cumulativity too.

Best,
Martin


On 09/07/13 20:15, Dan Licata wrote:
> Hi Martin,
>
> How would using such a system be different than implicit universe
> polymorphism, like was recently implemented in Coq?  It seems like a
> difference in perspective---"all type:type programs are good programs,
> but we can pick out the ones that level check", as opposed to "only the
> level-checking programs are good, but the user can act as if type:type
> and we can infer whether they do while type checking"---which could be
> helpful for designing a tool.  But from the users' perspective, what
> differences would you expect?
>
>  From a "how heavy is it to use" perspective, I think the main thing I
> dislike about Agda's current solution is the lack of cumulativity.
> Personally, I think types with lots of paramters look nicer if you just
> have one level parameter, rather than one for each independent type, and
> lots of "max"'es expressing the relationship between them.
> But I know there are issues with cumulativity in Coq.
>
> Alternatively, if Agda implicitly added quantifiers over dependencies
> like Twelf does,, at least I wouldn't have to write and read the levels
> as much.  In Twelf, if you have indices of a type that is reconstructed,
> those indicies are also quantified over.  For example:
>
> forall {A B} -> A -> B
>
> would mean
>
> forall {l1 l2 : Level} {A : Set l1} {B : Set l2} -> A -> B
>
> Though I know there are difference that make this difficult (like being
> able to supply implicit arguments explicitly in Agda).  So this is
> really me complaining about the state of the art without having a solution...
>
> -Dan
>
> On Jul02, Martin Escardo wrote:
>> NB. Their paper already passes the test, of the referees and mine and more
>> people - it is not in question. What is in question is whether there is a
>> general way of deciding whether uses of type-in-type are good as posed
>> above.
>
> And Agda -- we have done a version of this proof without type:type :)
>