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 18:38:35 CEST 2010
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
I must be missing something, why won't the same hidden-argument
resolution work for function application?
> 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/
>
More information about the Agda
mailing list