The Coq mailing list

[Benjamin Werner <benjamin.werner AT polytechnique.fr>]

     Hello,

I agree the answer given in the faq is probably somewhat awkward and 
oughts to be rewritten.

The example about the the two sorting algorithms should not be 
understood as "extentional equality is bad" but rather as a 
quick-to-understand  illustration of the fact that in an intentional 
world like type theory, it is not a trivial truth like in set theory.

Best wishes,


Benjamin



Le 11 févr. 05, à 22:40, Jason Hickey a écrit :

> Xavier Leroy wrote:
> > So, I don't quite see why functional extensionality "cannot be
> > accepted from a programming point of view", but the above
> > identification can...
>
> It does seem strange that the argument against function extensionality 
> would be based on computational complexity.  Another example might be
>
>    fst (e1, e2) = e1
>
> which "forgets" about an arbitrarily complex computation e2.  However, 
> if evaluation is lazy then the equivalence does hold (and Xavier's two 
> power functions are also equivalent).
>
> Function extensionality can of course be very useful.  For example, 
> suppose we interpret records as functions from labels to values.  The 
> encoding is elegant and has many nice properties.  Without 
> extensionality, statements like the following become very tedious to 
> prove.
>
>    { { r with x = 1 } with y = 2 } = { { r with y = 2 } with x = 1 }
>
> I think the user might be unhappy to find that he has to account for 
> the computational complexity of his record operations.  In any case, I 
> would expect that there are other arguments against function 
> extensionality.
>
> BTW, Constable and Crary have an explicit account of computational 
> complexity in type theory:
>
>    Computational Complexity and Induction for Partial Computable
>    Functions in Type Theory, Constable and Crary, 2002.
>    http://www.nuprl.org/documents/Constable/01complexity.html
>
> Jason
>
> --
> Jason Hickey                  http://www.cs.caltech.edu/~jyh
> Caltech Computer Science      Tel: 626-395-6568 FAX: 626-792-4257
> --------------------------------------------------------
> 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