[Agda] Level constraints

Nils Anders Danielsson nad at cse.gu.se
Thu Nov 14 23:02:04 CET 2013

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.


More information about the Agda mailing list