Why values can not be replaced with their extensionally equal values in an intensional system?

Question

Thomas Streicher states in Investigations into Intensional Type Theory(§Introduction p.5) that:

Although in Intensional constructive set theory (Intensional Type Theory) one can do most of the things one wants to do... certain theorems simply do not hold due to the lack of extensionality. A typical example is that from $t\in B a$ and $p\in Id A ab$ one is not allowed t conclude that $t\in Bb$ where $A$ is a type and $B$ is a family of types indexed over $A$.(But of course one is allowed to infer $t\in Bb$ from $t\in Ba$ and $a=b\in A$ !)

An almost similar thin is mentioned in Definition of extensional and propositional equality in Martin-Lof extensional type theory :

The (Id-DefEq) means that extensional equality is baked into the type system: if you have a type constructor 𝑇:((𝑥:𝑈)→𝑉)→𝖲𝖾𝗍 then you can use a value of type 𝑇 𝑓 in a context expecting 𝑇 𝑔 if 𝑓 and 𝑔 map equal inputs to equal outputs. Again this is not true in an intensional system, where 𝑓 and 𝑔 might be incompatible if they're syntactically different.

Why is that? Isn't it that two functions that are producing exactly same output for their inputs, equal? So why can't one be replaced with another in a context? What makes definitionally equal functions eligible to be replaced with each other, but not the extensionally equal ones?

Answer 1

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.

Answer 2

Supposing we have $a$ and $b$ of type $A$ and $p : \mathrm{Id}_A(a,b)$, there simply is not any rule of type theory that would allow you to replace $b$ with $a$ arbitrarily. So one answer is "because type theory does not let you do that", and if you think that it can be done, please show me how. But I suppose that is a non-answer, what you really are asking is why is type theory designed in such a strange way.

There are many ways to understand equality. Students of mathematics are typically taught only one, namely the equality arising from set theory and classical mathematics. This kind of equality is very intuitive and easily understood. But as you learn more mathematics, you begin to understand that sometimes two objects are not really equal, but are "kind of equal". For example, they could be isomorphic, or connected by a path. So it makes sense to look for other explanations of equality that capture the idea of a more "relaxed" equality.

In mathematics it makes a lot of sense to say that functions are equal if they produce the same outputs, but this is not so in computer science. For example, if functions $f$ and $g$ produce the same outputs, but one is much faster than the other, then it is useless for a computer scientist to consider them equal.

Type theory is a formal system which allows us to express these ideas. The identity type $\mathrm{Id}_A(a,b)$ is not necessarily the "true equality" (the only one that a student of classical mathematics knows about, and therefore calls it "true") of $a$ and $b$, it could be one of these other notions of equality that you learn about when you study homotopy theory and computer science.

For instance, one way to undertand $p : \mathrm{Id}_A(a,b)$ is to say that $p$ is some sort of a "path" from $a$ to $b$. That is, $a$ and $b$ are not "really equal", but there is a way to get from $a$ to $b$. And so, if $P :A \to \mathrm{Type}$, we certainly would not expect $P a$ and $P b$ to be "exactly the same", but rather that "there is a way to get from $P a$ to $P b$". Indeed, this goes under name transport and it follows from the rules for the identity type: given $p : \mathrm{Id}_A(a,b)$, there is a isomorphism of types $\mathrm{transport}_p : P a \to P b$.