michael
/
blog
1
0
Fork 0
Code Issues 1 Pull Requests Releases Wiki Activity
blog/src/content/posts/2023-09-15-equality.md

4.3 KiB
Raw Blame History

title date tags draft
Equality 2023-09-15T05:36:53.757Z
type-theory
true

When learning type theory, it's important to make a distinction between several kinds of "same"-ness. Whenever you talk about two things being equal, you'd want to qualify it with one of these in order to make it clear which you're referring to, since they're very different concepts.

  • Definitional, or judgmental equality. This is usually written with \equiv in math. If you see x \equiv y, this says "I've defined x and $y$ to be the same, so anytime you see x, you can replace it with y and vice versa."

    [!NOTE] Technically speaking, definitional and judgmental are two separate concepts but coincide in many type theories. You could think of multiple levels of equalities like this:

    • Does 2 equal 2? Yes. This is the same object, and equality is reflexive.
    • Does s(s(z)) equal 2? Well, typically this is how natural numbers are defined in type systems: 2 \equiv s(s(z)). By definition they are identical.
    • Does 1 + 1 equal 2? The operation + is a function, and requires a β-reduction to evaluate any further. This choice really comes down to the choice of the type theory designer; if you wanted a more intensional type theory, you could choose to not allow β-reduction during evaluation of identities. Most type theories do allow this though.

  • Propositional equality. This describes a value that potentially holds true or false. This is typically written = in math.

Helpful tips

  • You can talk about propositional equalities conditionally, like "if a equals b, then c is true". This kind of expression doesn't really make sense for judgmental equality, like in the following example:

    Suppose you made the judgment: x = 2. It makes no sense to then say "if $x$ equals 2, then c is true." You can just skip right to c is true, because you've defined it to be true, so it's useless even thinking about the case where it's false because that would be a part of a completely different world entirely.

  • Here's a concrete example of the difference between judgmental and propositional equality. Consider these 2 expressions:

    • 2 + 3 = 3 + 2
    • \forall x\ y \in \mathbb{N} . (x + y = y + x)

    In the first case, performing β-reduction on both terms reduces to $5 = 5$, which is definitionally equal by virtue of being the exact same symbol.

    In the second case however, β-reduction is impossible. Without a specific x or y, there's actually no way to reduce either side more. You would need some other constructs to prove it, such as induction.

  • Suppose you were expressing these concepts in a language like TypeScript. The analog of a judgment would be something like:

    type Foo = string;

    Any time you're using Foo, you really don't have to compare it with string, because just through a simple substitution you will get the same symbol:

    function sayHello(who: string) { console.log(`Hello, ${who}`); }
function run(foo: Foo) { sayHello(foo); }

    On the other hand, a propositional equality type might look something like this instead:

    class Equal<A, B> {
  private constructor() {}
  static refl<A>(): Equal<A, A> {}
}

    You could have a value of this type, and query on its truthiness:

    type TwoEqualsTwo = Equal<Two, 2>;

function trans<A, B, C>(x: Equal<A, B>, y: Equal<B, C>): Equal<A, C> {
  // magic...
}

Notation gotcha

The syntax we use in most math papers and other literature and the syntax we use for equalities in various dependently-typed programming languages are annoyingly different:

Math Agda Coq Idris
Judgmental x \equiv y x = y x := y x = y
Propositional x = y x ≡ y x = y x = y

Usually there'll be some other pre-fix way of writing the propositional equals in your language too. In Agda, it's Path {A} x y.

More reading