How abstraction and application are type-checked [Re: [Agda] Agda type inference oddity on functions]

[Thorsten Altenkirch]

>  \ (x : A) -> t  synthesizes a function type (x : A) -> ?B where the new meta-var is the type of t
>  @Thorsten: Thus, not all metavars come from holes in the input!

True, I always thought that we can think of \(x : A) -> t as \x -> t : (x : A) -> ?.

> 
> Thus, \ (x : _) and \ x behaved differently, which is unexpected and confusing to the outsider.  As we have seen by Alan's examples, there are cases where \ (x : _) works and \ x not.  Can it also be the other way round?
> 
> @Ulf: Could \x be treated as \(x : _) ? There seems to be some abandoned code "forcePi" that tried to do this...
> 
> When checking an application, it is similar to the \ x case, it expects the head to be a function type, postpones if this is not the case, but does not propagate the information that the head must be a function.
> This explains failure of x3.
> 
> The weirdness of x5 is explained as follows.  Here, Agda needs to check that
> 
>  f : A <= N -> N
> 
> so again, it has the information that A {_} is a function type and can use that to invert on F.
> 
> So, can we improve on the type checking of an application f a?
> Well if f is not yet known to be a function type, we cannot simply say that it should be (x : ?1) -> ?2 x, where ?1 is the type of a, because there might be omitted hidden arguments between f and a.  So it would be
> 
>  Delta -> (x : ?1 Delta) -> ?2 Delta x
> 
> where Delta is a telescope of hidden variables of unknown length.
> 
> Such a concept does not exist (yet) in the guts of Agda, so I guess the situation cannot be rectified easily.
> 
> Cheers,
> Andreas
> 
> 
> On Sep 28, 2010, at 4:06 PM, Alan Jeffrey wrote:
> 
>> On 09/28/2010 05:05 AM, Thorsten Altenkirch wrote:
>>>>>> 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.
>> 
>> Yes, but the odd thing is we can find a context C s.t. C[lambda x -> x] has unsolved metas, but C[isFun(lambda x -> x)] does not.
>> 
>> NAD says this is due to a planned future addition to Agda -- not every lambda will have function type (and ditto not every application will be of a function).
>> 
>> [...]
>> 
>>>> 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.
>> 
>> It's because F is a constructor-headed function, so the term inference algorithm deduces that F is invertable.  So once there's a constraint (F X == Y -> Z), this is enough to solve (X == true) and hence (Y == Z == Nat).
>> 
>> This trick is enough to code functions whose implicit arguments have default value in existing Agda, if only application constrained a term to be a function!
>> 
>>> Cheers,
>>> Thorsten
>> 
>> A.
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>> 
> 
> Andreas Abel  <><      Du bist der geliebte Mensch.
> 
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
> 
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda