The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

With eta-conversion in sums you get non-trivial and suprising identities 
in definitional equality.  For instance, for f : bool -> bool and x : bool,

  f (f (f x)) = f x

definitionally!  I think that is beyond the scope of definitional 
equality, which is (besides lack of simplicity and feasibility) another 
argument against eta-conversion for sums.

Cheers,
Andreas

On 28.08.12 7:41 PM, Andrew Cave wrote:
> On Tue, Aug 28, 2012 at 10:18 AM, Ryan Wisnesky 
> <ryan AT cs.harvard.edu>
>  wrote:
> > In the simply typed case, one might like eta-conversion for functions, 
> > products, and sums - three conversions in total.  In Coq 8.4, it looks like 
> > we now have eta for functions, and you're working on eta for products, so I'm 
> > wondering about the third conversion, eta for sums - is that possible or even 
> > sensible?
>
> There's two papers I know of on this topic:
>
> Altenkirch et al. Normalization by evaluation for typed lambda
> calculus with coproducts. LICS 2001.
>
> Balat, Di Cosmo, and Fiore. Extensional normalisation and
> type-directed partial evaluation for typed lambda calculus with sums.
> POPL 2004.
>
> So it's possible, but it strikes me as quite complex to implement.

--
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/