[Agda] Level constraints

[Martin Escardo]

AND: I would really, really love to have typical ambiguity in Agda.

Not only for my own selfish convenience, but more importantly for 
avoiding people resorting to type-in-type as a poor man's version of 
typical ambiguity. Very many people use type-in-type simply because 
typical ambiguity is not available. (E.g. Licata and Schulman's LICS 
paper this year, for the sake of readability (rightly in my opinion), 
but also many more other Agda developments I've seen).

I agree with you that one has to have control when one wishes to. But 
also I think, one has to have the ability to devolve control when one 
wishes too. I repeat the analogy of typical ambiguity with implicit 
arguments. Without implicit arguments, writing proofs in type theory 
*would be* unbearable. Similarly, without typical ambiguity, writing 
some proofs/definitions in type theory in Agda notation *is* unbearable 
(hence the emergence of the type-in-type crowd, which I haven't joined 
yet, but I am often tempted to).

Best,
Martin

On 14/11/13 22:05, Martin Escardo wrote:
> On 14/11/13 22:02, Nils Anders Danielsson wrote:
>> On 2013-11-14 20:53, Martin Escardo wrote:
>>> There is one more option, which I favour: Feferman's "typical
>>> ambiguity", with Harper's algorithm or similar.
>>
>> Harper and Pollack's algorithm? I omitted this algorithm, and other
>> methods that can be used to avoid writing things (like Twelf-style type
>> reconstruction for undeclared variables), because AFAICT they are (at
>> least partly) orthogonal to the issue raised in this thread.
>>
>> My personal preference is (currently) to use something that satisfies
>> (at least) the following criteria:
>>
>> * In "simple" cases I don't want to mention universe levels at all.
>>
>> * In more complicated cases it should be possible to express exactly
>>    what I mean.
>>
>> * The system shouldn't make decisions for me.
>>
>> * The implementation should be efficient.
>
> I thought I argued in the previous message that typical ambiguity,
> considered as a layer on top of what we have, precisely addresses the
> first three points. I have no idea about the last.
>
> Best,
> Martin
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda