[Agda] Agda type inference oddity on functions
Alan Jeffrey
ajeffrey at bell-labs.com
Tue Sep 28 16:06:19 CEST 2010
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.
More information about the Agda
mailing list