2
$\begingroup$

The equality relation $=$ can be represented as a type, just as any other propostion in the Curry-Howard correspondence.

I understand the sense in which the basic logical symbols $\land,\lor,\to, \forall, \exists,\neg$ correspond to type constructions, and the sense in which a proof that has a type is a program (e.g. a proof of $A\to B$ is a program that takes a proof of $A$ and outputs a proof of $B$).

But how is a proof of $a=b$ a program? What is the general idea here? I haven’t seen a clear explanation yet.

$\endgroup$
6
  • $\begingroup$ Are you familiar with how lambda expressions are used to represent proofs of (the positive partial fragment of) propositional logic? Because it all starts there. $\endgroup$
    – DanielV
    Oct 17, 2020 at 16:28
  • $\begingroup$ A proof of $a = b$ is a program that transforms $a$ and $b$ into a common expression using some given rewriting rules. $\endgroup$
    – Zhen Lin
    Oct 17, 2020 at 22:23
  • $\begingroup$ @DanielV, yes I am $\endgroup$
    – user56834
    Oct 18, 2020 at 3:32
  • $\begingroup$ @ZhenLin, that sounds like the kind of answer I'm looking for. Do you know of a more detailed explanation written somewhere? $\endgroup$
    – user56834
    Oct 18, 2020 at 3:32
  • $\begingroup$ No. This is just a heuristic. In reality the "meaning" of $a = b$ will depend on how $=$ in the type has been defined. $\endgroup$
    – Zhen Lin
    Oct 18, 2020 at 6:16

2 Answers 2

1
$\begingroup$

As Zhen Lin has mentioned in the comments, the specifics will depend on how you are interpreting $=$ in your type theory. Here I will outline how $=$ is handled in HoTT for concreteness, but you will see that once we have a fixed type representing equality, everything works how you would expect.

In HoTT, we add the following inference rule to our logic:

$$\frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a, b : A}{\Gamma \vdash a =_A b \text{ type}}$$

That is, for every type $A$, and for every two values $a,b : A$, we assert the existence of a type $a =_A b$. Values inhabiting this type are proofs that $a$ and $b$ are equal.

To talk about how values $p : a =_A b$ are programs, we will talk about their introduction/elimination rules. I'm going to play slightly fast and loose with my notation here to try and keep the rules legible. If you want the gory details, see the appendix in the HoTT book linked above.

There is only one introduction rule:

$$ \frac{\Gamma \vdash A \text{ type} \quad \Gamma \vdash a : A}{\Gamma \vdash \text{refl}_a : a =_A a}$$

There is always a proof $\text{refl}_a$ (for reflexivity) asserting that $a=a$.

The elimination rule is rather subtle. It forms the basis of what is called "path induction" in HoTT, and is a common source of confusion when getting started. I won't go into too much detail about these subtleties here, though.

$$ \frac{ \Gamma, p:a =_A b \vdash C(p) \text{ type} \quad \Gamma, a_0 : A \vdash c(a_0) : C(\text{refl}_{a_0}) }{ \Gamma \vdash \text{ind}_{=_A}(c) : C(p) } $$

This says that given any type family $C$ depending on $p : a =_A b$, if we can eliminate the only introduction rule, then we can eliminate the entire type. That is, if some $c(a_0) : C(\text{refl}_{a_0})$, then we can get a value $\text{ind}_{=_A}(c) : C(p)$ for any $p : a =_A b$ we like. Moreover, $\text{ind}_{=_A}$ satisfies the computation rule:

$$(\text{ind}_{=_A}(c))(\text{refl}_a) = c(a)$$

If it seems surprising to you that we get all of this expressivity by working only with $\text{refl}_a$, you're in good company. This is just the tip of the "subtlety" iceberg that I was referring to earlier. Intuitively, since $\text{refl}_a$ is the only constructor for an equality type, once we prove something for it, we've proven something for the whole equality type. This is analogous to proving something for every value in $\mathbf{1}$ by proving it for $\ast : \mathbf{1}$. The only difference is in our heads: We like to imagine $\ast$ as being the only element of $\mathbf{1}$, while it's easy for us to imagine multiple possible elements of $a =_A b$, especially since our only constructor is for $a =_A a$, which feels like a weaker condition. Of course, type theory doesn't care about our hang-ups. There are plenty of models of type theory with equality where $\text{refl}_a$ honestly is the only value of any equality type.

As for actually "computing" things with equality types, the obvious practicality of the rest of the lambda calculus breaks down somewhat. While we are technically programming, I'm not sure if there's any analogue of equality types that, say, a software engineer might care about. This is in stark contrast to other constructions in type theory, which correspond to algebraic datatypes (and which thus have obvious real-world computational applications we can point to). I'm sure somebody has thought of what these types can properly compute, but I'm not familiar with any literature on the subject.


I hope this helps ^_^

$\endgroup$
2
  • 2
    $\begingroup$ One might say that the point of HoTT is to make use of 'equality' for programming. For instance, you haven't really presented anything homotopy related; this is just how intensional type theory does equality. The odd thing there is that equality types are computationally relevant, but there are no interesting values. So, this seems like a mistake, and leads people to K and making equality irrelevant. HoTT does the opposite: add values so that we can say how things are 'equal' in non-trivial ways. Then the computational relevance of equality is not a mistake. $\endgroup$
    – Dan Doel
    Oct 20, 2020 at 0:39
  • $\begingroup$ That's a really good remark, thank you ^_^ $\endgroup$ Oct 20, 2020 at 0:40
0
$\begingroup$

The general idea behind proof-as-program is the same for all propositions-as-types.

You wrote:

a proof of A→B is a program that takes a proof of A and outputs a proof of B

I would rather write:

a proof of A→B is a program that takes a term of type A and outputs a term of type B

In the same way, a proof of $a=b$ is a program that takes the terms $a$ and $b$ and outputs a term of type $a=b$. Depending how equality is defined in your type theory, a term of $a=b$ might be different things, but that's another story...

In the idea behind proof-as-program, the program is computing on terms, not on proofs. From propositions-as-types you get proofs-as-terms, but a term with a variable is a program, thus you have terms-as-programs and therefore proofs-as-programs...

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.