Function extensionality: does it make a difference? why would one keep it out of the axioms?

Question

Yesterday I was shocked to discover that function extensionality (the statement that if two functions $f$ and $g$ on the same domain satisfy $f\left(x\right) = g\left(x\right)$ for all $x$ in the domain, then $f = g$) is not an axiom in the standard constructive logic of Coq. Of course, one can add it as an axiom in one's files, but it is not obviously available in any pre-defined tactics. I am left wondering...

1. What is the thinking behind considering function extensionality as foreign to the calculus of constructions? I thought that from a computational perspective, a function really is there to be applied to things, and cannot carry any more information than what it does to them (and its type). For a moment I suspected that Coq avoids function extensionality in order to allow applying results to models like arbitrary enriched categories whose internal homomorphisms carry some more information than plain morphisms. But this is not the case: Coq (since version 8.4) has a implementation of eta-expansion (saying that any function $f$ equals the function sending every $x$ in its domain to $f\left(x\right)$, provided the types are right). In an enriched category, this would pour any additional structure of an internal Hom down the drain. (I must say the eta-expansion in Coq feels rather weird, too -- it is triggered by the reflexivity tactic. I expected it to be a tactic on its own...) Having eta-expansion but no extensionality is seriously confusing: one can have $f\left(x\right) = g\left(x\right)$ for all $x$, and yet one cannot rewrite the $f\left(x\right)$ in "the function sending every $x$ to $f\left(x\right)$" as a $g\left(x\right)$. And there I thought the bound variable in a lambda term would be like the bound variable in a forall quantification?

2. On a more practical note (and more on-topic in MathOverflow), how much do the axiom of function extensionality and the (weaker) axiom of eta-expansion contribute to the strength of the logic? (At this point I have to admit that I don't really know the definition of the logic involved, so I'll just say I'm talking about the logic of Coq with no additional axioms assumed; it has so far been agreeing with my intuitive understanding of constructivism, until extensionality came along.) If I can define two terms $a$ and $b$ of type $\mathrm{nat}$ (natural numbers) and use function extensionality (resp. eta-reduction, both ways) to prove their equality, can I also do it without? If I can prove a (more complicated) statement using function extensionality, is there a way to transform it into a (possibly clumsier) statement which can be proven without function extensionality and which can be transformed into the former statement using some straightforward applications of function extensionality?

I'm sorry for logical naivety. The way I am posing the question, I fear it would qualify as soft; nevertheless I am pretty sure that there is some precise statements to be made here (or maybe just a reference to a textbook to be given).

Answer 1

I am going to draw heavily from Github discussion on HoTT book pull request 617.

There are different kinds of equality. Let us say that equality is "intensional" if it distinguishes objects based on how they are defined, and "extensional" if it distinguishes objects based on their "extension" or "observable behavior". In Frege's terminology, intensional equality compares sense and extensional equality compares reference.

To use Russell's example, intensionally the morning star and the evening star are clearly not the same (because their definitions are different), but they are extensionally the same because they both denote the same object (planet Venus). A more mathematical example is comparison of $x + y$ and $y + x$. These are extensionally equal, but intensionally differ because (the usual) definition of $+$ treats its arguments asymmetrically. It should be clear that two functions may be extensionally equal (have same behavior) even though they differ intensionally (have different definitions).

It is possible for two kinds of equality to coexist. Thus in type theory there are two equalities. The intensional one is called "judgmental" or "definitional equality" $\equiv$ and the extensional one is known as "propositional equality" $=$. Mathematicians are aware of $=$ as a "real thing" while they think of $\equiv$ as "formal manipulation of symbolic expressions" or some such.

We may control the two kinds of equality and the relationship between them with additional axioms. For instance, the reflection rule collapses $\equiv$ and $=$ by allowing us to conclude $a \equiv b$ from $a = b$ (the other direction is automatic). There are also varying degrees of extensionality of $=$. Without any extra axioms, $=$ is already somewhat extensional. For instance, we can prove commutativity of $+$ on natural numbers by induction in the form $x + y = y + x$, but we cannot prove $x + y \equiv y + x$. Function extensionality is an axiom which describes what constitutes an "observation" on functions: by saying that two functions are equal when they give equal values we are in essence saying that only values matter (but not for example the "running time" or some other aspect of evaluation). Another axiom which makes $=$ "more extensional" is the Univalence axiom.

It is hard to do mathematics without function extensionality, but type theorists have their reasons for not including it as an axiom by default. But before I explain the reason, let me mention that there is a standard workaround. We may introduce user-defined equalities on types by equipping types with equivalence relations. This is what Bishop did in his constructive mathematics, and this is what we do in Coq when we use setoids. With such user-defined equalities we of course recover function extensionality by construction. However, setoids are often annoying to work with, and they drag in technical problems which we would prefer to avoid. Incidentally, the setoid model shows that function extensionality does not increase the power of type theory (it is a model validating function extensionality built in type theory without function extensionality).

So why don't type theorist adopt function extensionality? If we want to have a type theory with nice properties, and a useful proof assistant, then $\equiv$ should be "easy" to deal with. Technically speaking, we would like a strongly normalizing $\equiv$. By assuming function extensionality we throw into type theory a new constant funext without explaining how it interacts with the process of strong normalization, and things break. Type theorists would say that we failed to explain the computational meaning of funext.

Consequently, Coq does not adopt function extensionality because that would lead to a lot of problems. Coq would not be able to handle $\equiv$ automagically anymore, and the whole system would just have worse behavior. Type theorists of course recognize that having a good computational explanation of function extensionality, and more generally of the univalence problem, would be extremely desirable. This is why the HoTTest open problem is to give a computational interpretation of the univalence axiom. Once this is accomplished, we ought to have at our disposal type systems and proof assistants which are much more natural from a mathematician's point of view. Until then, you can always assume funext as an axiom and work around the resulting complications. To see how this can be done, have a loot at the Funext axiom in the HoTT library.

[This P.S. is outdated after the question was edited.] P.S. The title of your question points to a common leap of reasoning from "not accepting function extensionality" to "denying function extensionality". While there are models in which function extensionality has counter-examples, one should be aware of the difference between "not accept" and "deny". (I am complaining because this sort of leap is often made about the law of excluded middle, and there it leads to absurdity.)

Answer 2

You will lose canonicity, which is - mathematically - not that much of a problem, but when you want to extract programs, you want it. The problem is that not every proof of equality reduces to reflexivity.

See also http://coq.inria.fr/cocorico/extensional_equality

Answer 3

This worried me a lot when I started using Agda, but I got used to it. I expect that the issues in Coq are similar. The basic point is that one should not think of equality as being so important. In classical mathematics equality is very basic, and we routinely use quotient sets to replace the statement "$a$ is equivalent to $b$" by the apparently simpler statement that the equivalence class of $a$ is equal to the equivalence class of $b$. However, in a constructive framework this is not very natural. You need to keep hold of the equivalence relation and remember the proof that $a\sim b$ as an additional piece of data which can itself be fed into other functions and so on. Most of the time you end up working with "setoids", ie sets equipped with a specified equivalence relation; very few interesting mathematical structures can be constructed without an equivalence relation creeping in somewhere. After a while you get used to the idea that equality is not much better than other equivalence relations. So you can introduce extensional equality as a new equivalence relation, and not worry about the fact that it is different from the intensional version.