patternMinor
Why values can not be replaced with their extensionally equal values in an intensional system?
Viewed 0 times
whycanreplacedwithequalsystemextensionallyvaluesnotintensional
Problem
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?
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?
Solution
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$.
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$.
Context
StackExchange Computer Science Q#112615, answer score: 6
Revisions (0)
No revisions yet.