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

Andreas Abel andreas.abel at ifi.lmu.de
Tue Sep 28 22:54:17 CEST 2010


On Sep 28, 2010, at 10:12 PM, Alan Jeffrey wrote:
>> Any ideas how to express the hidden argument stuff as constraints?
>
> If I was building the thing from the ground up, I'd make hidden  
> arguments part of functions, that is the primitive type is:
>
>  {x : T} (y : U) -> V
>
> with matching lambda and application syntax.  The main reason for  
> this is to make explicit when hidden arguments are being resolved,  
> e.g. you'd have:
>
>  nil : {A : Set} -> () -> (List A)
>
> and you could distinguish between:
>
>  nil -- still generic
>  nil() -- has been made monomorphic
>
> Currently, it's a complete mystery exactly when hidden arguments are  
> inserted.  Of course, this is completely non-backwards compatible,  
> so will probably have to go on the shelf.
>
> The slightly more compatible version would have to be a horrible  
> hack, something like as follows...
>
> First, distinguish syntactically between terms with and without  
> implicit arguments:
>
>  A, B, C ::= lambda [x] . A' | x | A' B | _
>  A', B', C' ::= lambda x . A | A [B] | Pi(x:A')B' | Pi[x:A']B' | ...
>
> Here writing [...] for implicit arguments, as we need to do some  
> horrid uncurrying to get from the surface {...} to the internal [...]:
>
>  \ {x} -> A  =def=  lambda [(x,y)] . A [y]
>  \ x -> A =def= lambda [()] . lambda x . A
>  A B =def= A [_] B
>  A {B} =def= lambda [x] . A [(B,x)]
>  ...
>
> etc.  At this point, we can conflate implicit and explicit  
> arguments, and do regular old constraint solving.
>
> All quite horrid, but I suspect any attempt to try to make this  
> nicer ends up introducing things like row expressions, row  
> variables, row metavariables, etc. etc.

Mmh, but that seems more promising than your "horrid" ;-) proposal.

With row variables, an unknown function type would be

   {r : ?R} -> (x : ?X) -> ?Y r x

where r is a variable of row type and ?R is a row type metavariable.

Has anyone tried this?



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

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/



More information about the Agda mailing list