Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club]eta-reduction in the convertibility rule of Coq

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club]eta-reduction in the convertibility rule of Coq


chronological Thread 
  • From: Benjamin Werner <Benjamin.Werner AT inria.fr>
  • To: Stefan Monnier <monnier AT iro.umontreal.ca>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club]eta-reduction in the convertibility rule of Coq
  • Date: Wed, 18 Oct 2006 19:29:22 +0200
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

For a long time I thought it was only because the need was not srong enough
to make the implementation move.

I realized recently, that it would actually cause some more serious problems.

(actually what follows was known for a while, it just took me time to
paste things together)

Coq's type theory has some subtyping, especially between sorts

Type1 \subset Type2 \subset Type3  etc

Currently this subtyping is covariant but not contra-variant. That is if A' is a subset of A
you do not have necessarly that

A -> B  is a subtype of A' -> B

But if you want eta to preserve subject reduction for eta, you need to be contra-variant:

if f : A -> B

\x:A'.(f x) is of type A' -> B, but reduces to f. So you need to have f : A' -> B.



Now, contra-variance is not necessarly a nice thing. For various technical/implmentation
issues, but also because it messes up the simple set-theoretical semantics.

Indeed, If A' is a subset of A, then the set of functions form A to B is not a subset of
the set of functions from A' to B. You need some coercion, which in turn makes the interpretation
of equality problematic, etc.


So although I spent much of my PhD worktime dealing with eta, I am not in favour
of adding it to Coq for the moment.

Cheers,


Benjamin





Le 18 oct. 06 à 17:01, Stefan Monnier a écrit :


Can someone explain to me (or point me to a paper explaining it) why Coq
doesn't include eta-conversion in its convertibility rule?

Every once in a while, I end up having to manually eta-expand some term to
get my code to type check. Not a big deal, admittedly, but not quite as
elegant as I'd like.


        Stefan

--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
          http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club





Archive powered by MhonArc 2.6.16.

Top of Page