[Agda] Level constraints
m.escardo at cs.bham.ac.uk
Thu Nov 14 23:20:16 CET 2013
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).
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.
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda