How abstraction and application are type-checked [Re: [Agda]
Agda type inference oddity on functions]
Alan Jeffrey
ajeffrey at bell-labs.com
Tue Sep 28 22:12:24 CEST 2010
On 09/28/2010 01:34 PM, Andreas Abel wrote:
> 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?
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.
Like you said though, this isn't exactly an easy change to make.
A.
>
> 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/
>
More information about the Agda
mailing list