The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

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