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

Tue Sep 28 20:34:06 CEST 2010

The real problem is that not everything is a constraint.  Typing,  
Equality, Emptyness are constraints.
Other tests are just done on the spot, so order matters indeed.

- insertion of hidden arguments is done on the spot, it cannot be  
delayed
- ... (more?)

Any ideas how to express the hidden argument stuff as constraints?

On Sep 28, 2010, at 7:43 PM, Alan Jeffrey wrote:

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

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/