[Agda] Pie in the sky

[Alan Jeffrey]

On 09/24/2010 11:49 AM, Samuel Gélineau wrote:
> 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:

Thank you thank you, you're such a lovely audience, mwah.

>> [...] 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.

Yes, but the default is provided by the *type* of f, not by the name of 
f, so when the type inference system deduces the type of f, this will 
cause new implicit arguments to be filled in, which may cause further 
type inference.

My unscientific gut feeling is that this will be very hard to decide, 
just because you can code up fragments of subtyping, and type inference 
and subtyping don't live together very well.

> 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.

Could be.  I'm still worried about nontermination.  Of course, we still 
know soundness, because type checking is terminating, and pragmatically 
there's not much difference between nontermination and trying to 
typecheck a model of category theory :-)

A.