We don't always want extentionality
In mathematics, a function is a relation between its inputs and its output. Two functions are equal if and only if they map the same outputs to the same inputs. But in computer science, we're often interested in descriptions of computations which we also call โfunctionsโ, where it matters how the outputs are calculated from the inputs. When we describe a computation in different ways, we want to have a way to distinguish between them.
There are different reasonable definitions of what it means for expressions to be equal (I discussed this a bit in a previous answer). Definitional equality, where two expressions are equal if they can be rewritten to each other, is one of the most fundamental ones. But even it is too coarse for some uses: if you rewrite an expression to one that calculates the same value but in a more efficient way, it's certainly equivalent in some sense (we don't want optimizing compilers to transform our programs into programs that don't do the same thing), but it's also not equivalent in some sense (if we use an optimizing compiler, it's because it does make some useful difference).
Intuitively speaking, definitional equality captures equivalence between functions (in the computer science term) that only requires knowledge of how computation works, and not of what objects they manipulate. A precise formalization of what this means would be very dependent on the details of the calculs, so let me explain that through an example. Suppose you model the integers as follows:
$$
\begin{align}
\mathtt{N} &::= \mathtt{0} \;\mid\; \mathtt{S} \: (x:\mathtt{N}) \\
\mathtt{Z} &::= (\mathord{\mathtt{+}} \mid \mathord{\mathtt{-}}) \; (x:\mathtt{N}) \\
\end{align}
$$
That is, a natural integer is either 0 or the successor of a natural integer, and a signed integer is a sign (-
or +
) and a natural integer. This is a common representation of integers which is convenient for many proofs, and convenient if slow for many computations. Suppose you have a function that returns an element of $\mathtt{Z}$. We might like to say that it doesn't matter whether the function returns +0
or -0
for a given input, since +0
and -0
both represent the same integer $0$. But +0
and -0
are distinct objects. The equality on the implementation type $\mathtt{Z}$ is finer than the equality on the intended denotational semantics in $\mathbb{Z}$. In mathematical terms, equality of denotations induces an equivalence on the implementations that is not equality. This extends to functions that manipulate such objects: you get a coarser equivalence if you allow switching between equivalent representations than if you don't.
Likewise, definitional equality on functions means that these mathematical functions are implemented by the same object (up to computation). It is finer than extensional equality.
Extensionality is independent of some theories
In many theories, extensional equality is not built in. You can have a perfectly fine theory, useful for many things, where it is impossible to prove that $f = g$ even though it's possible to prove that $\forall x, f(x) = g(x)$.
For example, in the calculus of inductive constructions, or in Coq which is built upon it, it's impossible to prove Streicher's K or functional extensionality. They can be added as axioms without making the logic inconsistent, and you may want to do that for certain developments, but you don't get them from the core theory. Streicher's axiom K is implied by the law of excluded middle (but functional extensionality isn't), but excluded middle is not always desirable.
Properties like the law of excluded middle and extensional equality of functions go against constructive logic, where you don't just know that things are true, you actually have a proof of them. Constructive logic maps well to computations via the Curry-Howard correspondence. The law of excluded middle doesn't have nice a compuational analog. In intuitionistic logic, if you have a proof of $A \vee B$, you can either get a proof of $A$ or a proof of $B$; the computational interpretation is that you have an discriminated union of A
and B
, and you look at the tag to see whether it's an A
or a B
. But in classical logic, given a proof of $A \vee B$, you don't necessarily know which one it is; so on the computation side, you have to make a non-deterministic choice between A
and B
.
Extensionality is inconsistent with some theories
Sure, you can add Streicher's axiom K or extensionality of functions to Coq. But axioms that are admissible in isolation may be inconsistent if you add them together. There's a diagram of what implies what in the Coq FAQ, showing that impredicative Set plus the law of excluded middle plus the axiom of unique choice is inconsistent (but I think that any two is consistent). I don't know which sets of โreasonable-lookingโ axioms are compatible with K or with functional extensionality.
Streicher's axiom K is in particular inconsistent with the univalence axiom which is a cornerstone of homotopy type theory. This means that for example you can't directly model HoTT in Idris, since K is derivable from Idris's pattern matching. I don't understand this theory well enough to give an intuitive explanation for this inconsistency.