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

[Andreas Abel]

I looked at the Agda type checker and want to add some clarifications  
here:

- Bidirectional type checking:  Agda does not do bidirectional  
checking (= type checking and type inference), it only does type  
checking, where checking against a metavar has similar results to type  
inference.  Still, bidirectional type checking is a metaphor that  
explains some of Agda's behavior.

As Nisse already pointed out, typed and untyped lambdas are treated  
differently.

   \ x -> t   expects to be checked against a function type.  If it  
does not get a function type (e.g., it is checked against a meta  
variable, the type checking problem is postponed, but no constraint is  
propagated that the type of \ x -> t must be a function type).
  This explains the failure of Alan's term x1.

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

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/