[Agda] Level constraints
m.escardo at cs.bham.ac.uk
Thu Nov 14 23:05:35 CET 2013
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.
More information about the Agda