[Agda] More universe polymorphism

[Martin Escardo]

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