The Coq mailing list

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

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