[Agda] Agda type inference oddity on functions

[Thorsten Altenkirch]

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

I guessed that you mean that it successfully infers a type using C-c C-d. isFun (lambda x ->  x) certainly has unresolved metas.

>> 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'd say that all the metavariables should come from terms which are left out in user programs. At least this is my understanding of type inference for languages like Agda.

It is sort of wrong to call Agda's elaboration, type-inference. In my view it should be called term inference, because what is inferred are terms which are left out by the user. These may happen to be types. I think this is a fundamentally different approach to typing then the one taken in conventional languages like Haskell even though it superficially looks similar.

Having said this, I am sure that there are odd bits in the actual implementation of Agda's elaboration, e.g.

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

I am rather surprised that (isFun f x) can be inferred. Can somebody explain to me why this is the case.

Cheers,
Thorsten
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20100928/7c8d1923/attachment.html