[Agda] More universe polymorphism

[Martin Escardo]

And: isn't this more or less what Coq currently does in its "universe 
consistency checking"?

On 10/07/13 00:32, Martin Escardo wrote:
> Dan,
>
> In particular, if what I propose can be successfully implemented, then
> you should be able to remove the pragma type-in-type from your LICS
> paper with Mike Shulman, and get your agda file to type-check, without
> any further modification.
>
> Martin
>
> On 09/07/13 21:25, Martin Escardo wrote:
>> 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 :)
>>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda