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

[Andreas Abel]

I found an example where untyped lambda succeeds but typed lambda fails:

module HiddenLambdaInsertion where

IdT = ({A : Set} -> A -> A)

data _==_ {A : Set2}(a : A) : A -> Set where
   refl : a == a

foo : ({X : Set1} -> X -> X == IdT -> Set) -> Set
foo k = k (\ x -> x) refl         -- succeeds

foo' : ({X : Set1} -> X -> X == IdT -> Set) -> Set
foo' k = k (\ (x : _) -> x) refl  -- fails

foo succeeds because type checking  \ x -> x : X is postponed first  
and can then, after X := IdT, insert a hidden lambda \ {X} before \ x.

foo' fails because the type of \ (x : _) -> x is inferred as ?X -> ?X  
which cannot be unified with {A : Set} -> A -> A.

So typed and untyped lambda cannot be unified into one concept unless  
we find a better heuristics of inserting hidden arguments and hidden  
abstractions.

@Alan: short response below.

On Sep 28, 2010, at 6:38 PM, Alan Jeffrey wrote:

> Thanks for going through the typechecker Andreas!
>
> On 09/28/2010 11:05 AM, Andreas Abel wrote:
> [...]
>> 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?
>
> It certainly is confusing :-)  I'd be surprised if there were cases  
> the other way round, as (AFAICT) \x just propogates fewer  
> constraints then \x:_ -- but then the typechecker always has  
> surprises for me!
>
>> @Ulf: Could \x be treated as \(x : _) ? There seems to be some
>> abandoned code "forcePi" that tried to do this...
>
> This would be very nice!
>
> [...]
>> 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.
>
> Hmm, do we really need to do this?  Can we not just say that in an  
> application A B we add the typings:
>
>  A : (x : ?1) -> (?2 x)
>  B : ?1
>
> This doesn't preclude A having hidden arguments, won't they get  
> resolved in the "usual fashion"?  A parallel example is something  
> like (A ++ B) which adds the typings:
>
>  A : List ?1
>  B : List ?1
>
> Now if later we discover that A actually has type {T} -> List U then  
> inferred arguments are added, replacing this occurrence of A, and  
> getting:
>
>  A {?2} : List U
>  B : List U
>  ?2 : T

Well, I doubt it works like this, I would rather expect to get a type  
error, because

   List ?1 != {T} -> List U

> I must be missing something, why won't the same hidden-argument  
> resolution work for function application?

Hidden Pi-abstractions are never inserted, and the inserting of hidden  
arguments and abstractions follows also a fragile heuristics.

>> Such a concept does not exist (yet) in the guts of Agda, so I guess
>> the situation cannot be rectified easily.
>>
>> Cheers,
>> Andreas
>
> A.
>
>>
>>
>> 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/
>>
>
>

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/