From 328680c54bdfbf73a589402a668efe112ab24009 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 15 Sep 2023 01:42:41 -0500 Subject: [PATCH] equality notes --- src/content/posts/2023-09-15-equality.md | 117 +++++++++++++++++++++++ src/styles/_colors.scss | 8 ++ src/styles/post.scss | 23 ++++- 3 files changed, 144 insertions(+), 4 deletions(-) create mode 100644 src/content/posts/2023-09-15-equality.md diff --git a/src/content/posts/2023-09-15-equality.md b/src/content/posts/2023-09-15-equality.md new file mode 100644 index 0000000..40ba312 --- /dev/null +++ b/src/content/posts/2023-09-15-equality.md @@ -0,0 +1,117 @@ +--- +title: Equality +date: 2023-09-15T05:36:53.757Z +tags: + - type-theory +draft: 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: + + ```ts + 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: + + ```ts + class Equal { + private constructor() {} + static refl(): Equal {} + } + ``` + + You could have a value of this type, and query on its truthiness: + + ```ts + type TwoEqualsTwo = Equal; + + function trans(x: Equal, y: Equal): Equal { + // 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 + +- https://ncatlab.org/nlab/show/definitional+equality +- https://ncatlab.org/nlab/show/judgment +- https://ncatlab.org/nlab/show/judgmental+equality +- https://hott.github.io/book/hott-ebook.pdf.html diff --git a/src/styles/_colors.scss b/src/styles/_colors.scss index 77f94b7..7eb4af9 100644 --- a/src/styles/_colors.scss +++ b/src/styles/_colors.scss @@ -18,6 +18,10 @@ --code-color: firebrick; --tag-color: #{lighten($linkColor, 35%)}; + // Admonition + --note-color: #{$linkColor}; + --note-background-color: var(--link-hover-color); + // Syntax Highlighting --astro-code-color-text: #24292e; --astro-code-color-background: inherit; @@ -53,6 +57,10 @@ --code-color: #{lighten(firebrick, 25%)}; --tag-color: #{darken($linkColor, 55%)}; + // Admonition + --note-color: #{$linkColor}; + --note-background-color: var(--link-hover-color); + // Syntax Highlighting --astro-code-color-text: #e1e4e8; --astro-code-color-background: inherit; diff --git a/src/styles/post.scss b/src/styles/post.scss index 05d9939..d04976f 100644 --- a/src/styles/post.scss +++ b/src/styles/post.scss @@ -39,6 +39,11 @@ display: none; } + p, + ul { + margin-block: 12px; + } + p > img { max-width: 100%; height: auto; @@ -250,17 +255,27 @@ hr.endline { .admonition { // TODO: Figure out how to distinguish admonitions - --color: var(--link-color); + --admonition-color: var(--note-color); - border-left: 4px solid var(--color); - padding-left: 8px; + background-color: var(--note-background-color); + border-left: 4px solid var(--admonition-color); + padding: 8px; font-size: 0.9rem; + border-radius: 8px; .admonition-title { - color: var(--color); + color: var(--admonition-color); } p { margin: 8px auto; } + + :first-child { + margin-top: 0; + } + + :last-child { + margin-bottom: 0; + } }