The Coq mailing list

[Jason Hickey <jyh AT cs.caltech.edu>]

jean-francois.monin AT imag.fr
 wrote:
> The relation with time complexity is not very clear here since
> mergesort and quicksort are both O(n*log n) "in most practical
> cases". They are just completely different algorithms.

Of course.  I had assumed that if one cared about the difference between 
mergesort and quicksort, then one might also care about the difference 
between mergesort and bubblesort:)

Seriously though, I'm curious why Coq does not admit function 
extensionality.  The PRL (Martin-Lof-style) type theories are carefully 
intensional with two exceptions--the function type is fully extensional, 
and the quotient type is partially extensional.

Function and quotient extensionality are wonderful to work with--they 
tend to enhance reasoning, rather than compromising it as most 
extensional types would (for instance, an extensional Prop can be very 
hard to work with).

Certainly, function extensionality abandons any hope of preserving 
computational complexity.  But type theory is not designed so that 
equality preserves complexity!  If you want that, abandon CoIC, and use 
a Fefferman-style type theory where equality is alpha-equality.

The PRL theories are different from CoIC of course.  In PRL, type 
membership is undecidable (in CoC it is decidable), but in PRL general 
recursion is fine (CoC only allows primitive recursion).  These 
tradeoffs are behind an obscure trans-Atlantic type-theoretic feud:)

But, let me throw down the guantlet.  Why are the Coq folks so backward 
as to refuse function extensionality?  If there are technical reasons, 
why not be clear about it, and define a standard theory extension for 
people who care about reasoning, not complexity?

Jason

--
Jason Hickey                  http://www.cs.caltech.edu/~jyh
Caltech Computer Science      Tel: 626-395-6568 FAX: 626-792-4257