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

[Alan Jeffrey]

Looks like I'm treading into dangerous water here...

On 09/28/2010 12:12 PM, Andreas Abel wrote:
> I found an example where untyped lambda succeeds but typed lambda fails:

Oh my goodness.  Er, doesn't this mean there's a horrible race condition 
in the unification engine?  For example, swapping the order of arguments 
to foo' gives:

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

which looks to me that the order of constraint evaluation is making a 
difference, so constraint solving isn't Church-Rosser!

A.

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