[Agda] eta expansion

[Andreas Abel]

Hello Martin,

you might wanna talk to Andres Sicard-Ramirez who very recently asked a 
similar question on this list.

A principal difficulty is that higher-order unification is easier to 
implement with eta.  In Agda, a meta variable of type B created in 
context x:A becomes

   X x

where X : (x:A) -> B.  It is not distinguished from a meta variable Y of 
type (x:A) -> B in the empty context.  This would not be sound if we had 
not eta.

Also, consider the following example

postulate
   A : Set
   f : A → A

test :
   let Y : A -> A
       Y = _
   in  ((x : A) → Y x ≡ f x) × (Y ≡ f)
test = (λ x → refl) , refl

test2 :
   let Y : A -> A
       Y = _
   in  ((x : A) → Y x ≡ f x) × (Y ≡ λ x → f x)
test2 = (λ x → refl) , refl

Without eta, the equation Y x == f x gives two different solutions for 
Y: f and \lambda x -> f x.  It is not clear which one Agda should 
choose, one of the tests would fail, and it would be rather arbitrary.

Cheers,
Andreas

On 08.03.2013 15:46, Martin Escardo wrote:
> Is it possible to disable the eta expansion for definitional equality in
> Agda?
> _______________________________________________
> 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/