coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club]eta-reduction in the convertibility rule of Coq, Stefan Monnier
- Re: [Coq-Club]eta-reduction in the convertibility rule of Coq, Benjamin Werner
Archive powered by MhonArc 2.6.16.