[Agda] Agda type inference oddity on functions

[Alan Jeffrey]

Hmm, evidently I should have been clearer about what I meant...

On 09/27/2010 12:58 PM, Thorsten Altenkirch wrote:
> Hi Alan,
>
>>
>> An issue in the context of being able to implement functions with default values for implicit parameters (the "Pie In The Sky" thread). There may be a roadblock, caused by some odd behaviour around when Agda can infer that a term has function type.
>>
>> Attached is a program that defines a function whose only effect is to enforce that its argument is a function.  The version in the file is level-polymorphic and deals with dependent functions, but its simpler cousin is:
>>
>>   isFun : {A B : Set} ->  (A ->  B) ->  (A ->  B)
>>   isFun f = f
>>
>> Then we can show that there are contexts such that:
>>
>> a) isFun (lambda x ->  x) type-infers, but (lambda x ->  x) does not.
>
> What does "type-infers" mean?

I mean "accepted by the Agda type-checker without unsolved metas", or 
more concretely no yellow ink in agda-mode.

> Which type should (lambda x ->  x) infer to?

In this example, I was expecting the type inference algorithm to 
introduce a new meta, and give (lambda x -> x) the type (X -> X).  In 
the example code, that's enough information for the rest of the program 
to typecheck.

> I guess you are thinking of {A : Set} ->  A ->  A? But this would mean that type inference also has to insert a lambda abstraction. This would be odd.

Nope, I was thinking (X -> X) for a new meta X.

>> b) (isFun f x) type-infers, but (f x) does not.
>
> You didn't tell us what f and x are?

In the example, they're variables, of rather weird type.  The type of f is:

   {b : bool} -> (F b)

where:

   F true = (Nat -> Nat)
   F false = Nat

So the oddness is that (isFun f x) is inferred correctly to be (isFun (f 
{true}) x), but (f x) ends up as (f {Z} x) for an unsolved meta Z. 
AFAICT this is because the inference algorithm doesn't infer a function 
type for f, even though it's been applied!

>> That is, the type inference engine doesn't infer that lambda-terms or applied terms have function type, which seems odd to me.
>
> To understand Agda, I think it is best first to understand the type checking process (i.e. without any existential variables) - what is called type inference is simply obtained by replacing the terms which the user omitted by existential variables (and these may be any terms not just typed).
> I.e.
>
> (isFun f x)
>
> really means
>
> (isFun {?} {?} f x)
>
> hence it "infers" to ? ->  ?.

Indeed.  Being even more explicit about the metas, and the types being 
assigned to terms, (isFun f x) is inferred to be:

   f : X -> Y
   x : X
   (isFun {X} {Y} f x) : Y

However, I'd expect a similar assignment without the isFun:

   f : X -> Y
   x : X
   f x : Y

I hope this is a bit clearer!

A.

> The definition of type checking (w.o. any variables) is itself "bidirectional" and is decomposed in check and infer. E.g. variables and application can be infered while lambda abstractions can only be checked. Hence isFun applied to something can be infered, while (\ x ->  x) cannot. What should it be?
>
> I don't understand what you mean by "f x" cannot be inferred. It clearly can if I know something about f and x.
>
> I think one has to be a bit careful with preconceptions from Haskell or similar languages. I always thought there where a bit odd because type inference isn't clearly based on type checking but the type inferencer is allowed to play all sort of tricks. I don't think this would work so well for Agda.
>
>> Also, eta-expansion can cause terms to fail to type-infer, that is there are types such that:
>>
>>   ok : A ->  B ->  C
>>   ok f = f -- type-infers
>>
>>   nok : A ->  B ->  C
>>   nok f x = f x -- fails
>>
>> Bug, or feature?  (I had a look in the issue-tracker, didn't find it there...)
>
> Clearly, feature I'd say. you haven't said what the problem is actually.
>
> Cheers,
> Thorsten
>
>>
>> A.
>> <Odd.agda>_______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>