[Agda] eta-equality for records and metavar resolution
Christian Sattler
sattler.christian at gmail.com
Sat Dec 28 13:44:27 CET 2013
Hi Andreas,
Good to know a fix has been proposed! The type of situations where I
encounter this issue is actually fairly common when reasoning about
dependent sums or products where the first type parameter is itself a
Σ-type. One example is associativity of Σ (when the right-hand side is
left implicit):
Σ (Σ A B) (λ {(a , b) → C a b}) ≃ Σ A (λ a → Σ (B a) (C a))
Cheers,
Christian
On 2013-12-28 13:11, Andreas Abel wrote:
> Hi Christian,
>
> good for bringing this up! This is a known issue:
>
> http://code.google.com/p/agda/issues/detail?id=376
>
> With Brigitte did the necessary research to fix this, see our TLCA
> 2011 paper.
>
> However, I was wondering if this issue shows up in practice. (See
> comment #6.) Apparently, you got stuck on it, so it seems worthwhile
> fixing.
>
> A fix seems to be: Whenever we see a meta-variable applied to a
> projected variable, we rewrite the context such that the projected
> variable is replaced by a "tuple" of fresh variables of the
> appropriate types. More precisely, we solve the meta-variable by a
> new one which lives in the thus expanded context.
>
> Cheers,
> Andreas
>
> On 26.12.13 10:19 PM, Christian Sattler wrote:
>> Hi everyone,
>>
>> Given (A B : Set), abbreviate
>>
>> T = {C : A → B → Set} → Σ (A × B) (λ {(a , b) → C a b}).
>>
>> Given an occurrence of a variable (t : T), one would like the implicit
>> parameter C to be resolvable from a given value for the resulting type Σ
>> (A × B) (λ {(a , b) → C a b}) of the same shape: records are specified
>> to have eta-conversion after all. We can test this hypothesis as
>> follows:
>>
>> f : T → T
>> f t = t
>>
>> Alas, the implicit argument C of t will be marked unresolved: the
>> contraint resolver gets stuck at
>>
>> _C_11 (π₁ x) (π₂ x) =< .C (π₁ x) (π₂ x) : Set.
>>
>> Why is that? Should eta-expansion not allow us to regard x as a pair (a
>> , b), which would simplify the contraint to _C_11 a b =< .C a b?
>>
>> Ironically, the situation changes if we choose
>>
>> T = {C : A × B → Set} → Σ (A × B) (λ {(a , b) → C (a , b)})
>>
>> (but not with B × A!) - because of eta!
>>
>> Cheers,
>> Christian
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
More information about the Agda
mailing list