The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Indeed I meant "eta-reduction is unsound in Coq", but part of the sentence. Hugo Herbelin's slide explains the issue very well (it is indeed very specific to technical choices in Coq). Thanks Robbert.

That said, Coq doesn't really have eta-expansion, in that if you compute the normal form of a term, it won't be eta-long. In the conversion algorithm, eta-expansion is treated lazily as far as I understand (when comparing an abstraction to a term which isn't one). The conversion algorithm is untyped, but doint eta this way ensures well-typedness.

On 16 November 2012 13:14, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

On 11/16/2012 01:08 PM, AUGER Cédric wrote:

What do you mean by 'eta-reduction' is unsound?

It makes confluence and subject reduction fail in the presence of subtyping. See slide 24 of http://pauillac.inria.fr/~herbelin/talks/cic.pdf. That is why Coq has (typed) eta-expansion instead.

Robbert