[Agda] Agda type inference oddity on functions

[Thorsten Altenkirch]

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?

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

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.

> b) (isFun f x) type-infers, but (f x) does not.

You didn't tell us what f and x are?

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

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