The Coq mailing list

[roconnor AT theorem.ca]

On Sat, 12 Feb 2005, Jason Hickey wrote:

> 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.
>
> [...]
>
> 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?

Presumably extensionality would break strong normalization?  And without
strong normalization doesn't (dependant) type-checking break?  I think
this is a case, but I am not an expert on these things.

Intensionality has never prevented me from proving something that I have
wanted to prove, although it has made some proofs more difficult.  Of
course, perhaps thinking intensionally has perhaps coloured my view on
what I want to prove.

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''