[Agda] More universe polymorphism

[Martin Escardo]

On 06/08/13 03:14, Dan Licata wrote:
> Just got back to this thread, but I agree that what you said would be
> nice, and that it's what coq does.   -Dan

I wonder how difficult would be to incorporate a pragma for typical 
ambiguity in Agda (compatible with the current universe handling, and 
not necessarily including universe coersion).

Martin


>
> On Jul10, Martin Escardo wrote:
>> 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
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda