[Agda] Pie in the sky

[Samuel Gélineau]

On 2010-09-24 at 10:38 AM, Alan Jeffrey wrote:
>  f : (x y : T) -> {x==y ? refl : x == y} -> U
>
> so in the common case, we can call (f x x) and have "refl" inferred as the
> default.

What a great idea!! Again, barring an obvious and true reason why this
could never work, I'd volunteer to implement that. Speaking of which:

> [...] I'd bet good money on it
> (and indeed any similar proposal for default values) to cause type inference
> to diverge.  Type checking on fully-inferred code will still terminate, but
> that may not be much use if type inference doesn't.

Why would this interfere with type inference? Since duplicate
non-constructor names are not allowed, the compiler can probably
lookup f's definition before doing any type-inference. At this point
it can transform (f x y) into (f x y {refl}) and obtain a plain Agda
program on which type-inference will work as it always did.

I can imagine there might be problems with defaults in constructor
types and with partially-applied calls like (f x), but the initial
implementation could just forbid these cases and it would still be a
huge step forward.


with renewed enthusiasm,
– Samuel