From afaec7c0b6a6bd2bcff82ca070ed0c3172a698a5 Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Fri, 21 Apr 2023 01:18:34 -0500 Subject: [PATCH] Write some more --- assets/sass/_content.scss | 17 +- assets/sass/main.scss | 4 +- .../posts/2023-04-20-programmable-proofs.md | 394 +++++++++++++----- 3 files changed, 300 insertions(+), 115 deletions(-) diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss index 126d000..5baeaa0 100644 --- a/assets/sass/_content.scss +++ b/assets/sass/_content.scss @@ -463,24 +463,31 @@ table.table { min-width: 1px; details { - border: 1px solid lightgray; + border: 1px solid $hr-color; // padding: 10px 30px; font-size: 0.9rem; padding: 0 30px; line-height: 1.5; + p:nth-of-type(1) { + padding-top: 0; + margin-top: 0; + } + summary { padding: 10px 0; + transition: margin 150ms ease-out; } &[open] summary { - border-bottom: 1px solid lightgray; + border-bottom: 1px solid $hr-color; + margin-bottom: 15px; } } hr { border-width: 1px 0 0 0; - border-color: $faded-background-color; + border-color: $hr-color; margin: 32px auto; width: 20%; } @@ -570,8 +577,8 @@ table.table { } } -.endline { +hr.endline { margin-top: 30px; border-width: 1px 0 0 0; - border-color: $faded-background-color; + border-color: $hr-color; } diff --git a/assets/sass/main.scss b/assets/sass/main.scss index 1c547d7..0a72e2d 100644 --- a/assets/sass/main.scss +++ b/assets/sass/main.scss @@ -20,6 +20,7 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline", $small-text-color: #6e707f; $smaller-text-color: lighten($text-color, 30%); $faded: lightgray; + $hr-color: lightgray; $link-color: royalblue; $code-color: firebrick; $tag-color: lighten($link-color, 35%); @@ -29,13 +30,14 @@ $monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline", @media (prefers-color-scheme: dark) { $background-color: #202030; - $faded-background-color: lighten($background-color, 30%); + $faded-background-color: lighten($background-color, 10%); $shadow-color: lighten($background-color, 10%); $heading-color: lighten(lightskyblue, 20%); $text-color: #CDCDCD; $small-text-color: darken($text-color, 8%); $smaller-text-color: darken($text-color, 12%); $faded: #666; + $hr-color: gray; $link-color: lightskyblue; $code-color: lighten(firebrick, 25%); $tag-color: darken($link-color, 55%); diff --git a/content/posts/2023-04-20-programmable-proofs.md b/content/posts/2023-04-20-programmable-proofs.md index 3055971..4c0dbf9 100644 --- a/content/posts/2023-04-20-programmable-proofs.md +++ b/content/posts/2023-04-20-programmable-proofs.md @@ -12,27 +12,26 @@ entire proof system on top of a programming language and verify mathematical statements purely with programs. To make this idea more approachable, I'm going to stick to using [Typescript] -for the majority of my examples, to explain the concepts. I personally love the -way this language tackles a type system, and even though there are certain -things it lacks, I still find it generally useful and intuitive for talking -about basic ideas. +for some of the starting examples to explain the concepts. Then, we'll go and +see how this stacks up in a language designed for writing mathematical proofs. --- -Let's start with a very simple data type: a class! We can make new classes in -Typescript like this: +If we're going to talk about type theory, let's start by bringing some types to +the table. In Typescript, there's a very simple way to create a type: defining a +class! We can make new classes in Typescript like this: ```ts class Cake {} ``` -That's all there is to it! `Cake` is now a full-fledged data type. What does -being a data type mean? +Simple enough. `Cake` is a type now. What does being a type mean? - We can make some `Cake` like this: ```ts - let cake = new Cake(); + let cake1 = new Cake(); + let cake2 = new Cake(); ``` - We can use it in function definitions, like this: @@ -44,10 +43,14 @@ being a data type mean? - We can put it in other types, like this: ```ts - type Party = { cake: Cake, balloons: Balloons, ... }; + type Party = { cake: Cake, balloons: Balloon[], ... }; ``` -Ok that's cool. But what about classes with no constructors? + This creates a `Party` object that contains a `Cake`, some `Balloon`s, and + possibly some other things. + +Ok that's cool. But we're curious people, so suppose we decide to have some fun +and make a class that doesn't have a constructor: ```ts class NoCake { @@ -55,102 +58,122 @@ class NoCake { } ``` -In Typescript and many OO languages it's based on, classes are given -public constructors by default. This lets anyone create an instance of the -class, and get all the great benefits we just talked about above. But when we -lock down the constructor, we can't just freely create instances of this class -anymore. +> I admit, there still is a constructor, but just a private one, which means you +> can't call it from outside the class. Same thing in effect. + +In Typescript and many OO languages it's based on, classes are given public +constructors by default. This lets anyone create an instance of the class, and +get all the great benefits we just talked about above. But when we lock down the +constructor, we can't just freely create instances of this class anymore.
Why might we want to have private constructors? - Let's say you had integer user IDs, and in your application whenever you wrote - a helper function that had to deal with user IDs, you had to first check that - it was a valid ID: +Let's say you had integer user IDs, and in your application whenever you wrote +a helper function that had to deal with user IDs, you had to first check that +it was a valid ID: - ```ts - function getUsername(id: number) { +```ts +/** @throws {Error} */ +function getUsername(id: number): string { + // First, check if id is even a valid id... + if (!isIdValid(id)) throw new Error("Invalid ID"); + + // Ok, now we are sure that id is valid. + ... +} +``` + +It would be really nice if we could make a type to encapsulate this, so that +we know that every instance of this class was a valid id, rather than passing +around numbers and doing the check every time. + +```ts +function getUsername(id: UserId): string { + // We can just skip the first part entirely now! + // Because of the type of the input, we are sure that id is valid. + ... +} +``` + +Note that the function also won't throw an exception for an invalid id +anymore! That's because we're moving the check somewhere else. You could +probably imagine what an implementation of this "somewhere else" looks like: + +```ts +class UserId { + private id: number; + + /** @throws {Error} */ + constructor(id: number) { // First, check if id is even a valid id... if (!isIdValid(id)) throw new Error("Invalid ID"); - // Ok, now we are sure that id is valid. - ... + this.id = number; } - ``` +} +``` - It would be really nice if we could make a type to encapsulate this, so that - we know that every instance of this class was a valid id, rather than passing - around numbers and doing the check every time. +This is one way to do it. But throwing exceptions from constructors is +typically bad practice. This is because constructors are meant to be the final +step in creating a particular object and should always return successfully and +not have side effects. So in reality, what we want is to put this into a +_static method_ that can create `UserId` objects: - ```ts - function getUsername(id: UserId) { - // We can just skip the first part entirely now! - // Because of the type of the input, we are sure that id is valid. - ... +```ts +class UserId { + private id: number; + constructor(id: number) { + this.id = id; } - ``` - You could probably imagine what an implementation of this type looks like: - - ```ts - class UserId { - private id: number; - - /** @throws {Error} */ - constructor(id: number) { - // First, check if id is even a valid id... - if (!isIdValid(id)) throw new Error("Invalid ID"); - - this.id = number; - } + /** @throws {Error} */ + fromNumberChecked() { + // First, check if id is even a valid id... + if (!isIdValid(id)) throw new Error("Invalid ID"); + return new UserId(id); } - ``` +} +``` - This is one way to do it. But throwing exceptions from constructors is - typically bad practice. This is because constructors are meant to be the final - step in creating a particular object and should always return successfully and - not have side effects. So in reality, what we want is to put this into a - _static method_ that can create `UserId` objects: +But this doesn't work if the constructor is also public, because someone can +just **bypass** this check function and call the constructor anyway with an +invalid id! We need to limit the constructor, so that all attempts to create +a `UserId` instance goes through our function: - ```ts - class UserId { - private id: number; - constructor(id: number) { this.id = id; } - - /** @throws {Error} */ - fromNumberChecked() { - // First, check if id is even a valid id... - if (!isIdValid(id)) throw new Error("Invalid ID"); - return new UserId(id); - } +```ts +class UserId { + private id: number; + private constructor(id: number) { + this.id = id; } - ``` - But this doesn't work if the constructor is also public, because someone can - just **bypass** this check function and call the constructor anyway with an - invalid id! We need to limit the constructor, so that all attempts to create - a `UserId` instance goes through our function: - - ```ts - class UserId { - private id: number; - private constructor(id: number) { this.id = id; } - - /** @throws {Error} */ - fromNumberChecked() { - // First, check if id is even a valid id... - if (!isIdValid(id)) throw new Error("Invalid ID"); - return new UserId(id); - } + /** @throws {Error} */ + fromNumberChecked() { + // First, check if id is even a valid id... + if (!isIdValid(id)) throw new Error("Invalid ID"); + return new UserId(id); } - ``` +} +``` + +Now we can rest assured that no matter what, if I get passed a `UserId` +object, it's going to be valid. + +```ts +function getUsername(id: UserId): string { + // We can just skip the first part entirely now! + // Because of the type of the input, we are sure that id is valid. + ... +} +``` + +This works for all kinds of validations, as long as the validation is +_permanent_. So actually in our example, a user could get deleted while we +still have `UserId` objects lying around, so the validity would not be true. +But if we've checked that an email is of the correct form, for example, then +we know it's valid forever. - Now we can rest assured that no matter what, if I get passed a `UserId` - object, it's going to be valid. This works for all kinds of validations, as - long as the validation is _permanent_. So actually in our example, a user - could get deleted while we still have `UserId` objects lying around, so the - validity would not be true. But if we've checked that an email is of the - correct form, for example, then we know it's valid forever.
Let's keep going down this `NoCake` example, and suppose we never implemented @@ -160,7 +183,7 @@ create an instance of this class_. But what about our use cases? -- We can no longer make `NoCake`. This produces a code visibility error: +- We can no longer make `NoCake`. This produces a method visibility error: ```ts let cake = new NoCake(); @@ -175,7 +198,7 @@ But what about our use cases? ```ts function giveMeCake(cake: NoCake) { ... } - type Party = { cake: NoCake, balloons: Balloons, ... }; + type Party = { cake: NoCake, balloons: Balloon[], ... }; ``` Interestingly, this actually still typechecks! Why is that? @@ -189,7 +212,9 @@ But what about our use cases? later on. Think about what happens to `Party` if one of its required elements is something that can never be created. - No cake, no party! The `Party` type _also_ can't ever be constructed. + No cake, no party! The `Party` type _also_ can't ever be constructed. The + _type_ called `Party` still exists, we just can't produce an object that will + qualify as a `Party`. We've actually created a very important concept in type theory, known as the **bottom type**. In math, this corresponds to $\emptyset$, or the _empty set_, @@ -198,23 +223,12 @@ but in logic and type theory we typically write it as $\bot$ and read it as What this represents is a concept of impossibility. If a function requires an instance of a bottom type, it can never be called, and if a type constructor -requires a bottom type, it can never be constructed. - -> Aside: in type theory, type constructors like structs and generics are really -> just Type $\rightarrow$ Type functions, so you could also think of it as a -> function as well. The difference is that the type constructor can actually -> succeed. I can write this type: -> -> ```ts -> type NoCakeList = NoCake[]; -> ``` -> -> But because I can never get an instance of `NoCake`, I can also never get an -> instance of `NoCakeList`. +requires a bottom type, like `Party`, it can never be constructed. Typescript actually has the concept of the bottom type baked into the language: -[`never`][never]. It's used to describe computations that never produce a value. -For example, consider the following functions: +[`never`][never]. So we never actually needed to create this `NoCake` type at +all! We could've just used `never`. It's used to describe computations that +never produce a value. For example, consider the following functions: ```ts // Throw an error @@ -224,7 +238,9 @@ function never1(): never { // Infinite loop function never2(): never { - while (true) { } + while (true) { + /* no breaks */ + } } ``` @@ -239,10 +255,170 @@ function usingNever() { ``` You can _never_ assign a value to the variable `canThisValueExist`, because the -program will never reach any of the statements after it. The `throw` will bubble -up and throw up before you get a chance to use the value after it, and the -infinite loop will never even finish, so nothing after it will get run. +program will never reach the log statement, or any of the statements after it. +The `throw` will bubble up and throw up before you get a chance to use the value +after it, and the infinite loop will never even finish, so nothing after it will +ever get run. + +We can actually confirm that the `never` type can represent logical falsehood, +by using one of the "features" of false, which is that ["false implies +anything"][false]. In code, this looks like: + +```ts +function exFalso(x: never): T { + return x; +} +``` + +You'll notice that even though this function returns `T`, you can just return +`x` and the typechecker is satisfied with it. Typescript bakes this behavior +into the subtyping rules of `never`, so `never` type-checks as any other type, +so for example you can't do this easily with our `NoCake` type. + +```ts +// Does not type-check! +function notExFalso(x: NoCake): T { + return x; +} +``` + +Ok, we've covered bottom types, and established that it's analogous to logical +falsehood. But what represents logical truth? + +Well, here's where we have to talk about what truth means. There's two big +parties of logical thought that are involved here. Let's meet them: + +- **Classical logic**: gets its name from distinguishing itself from + intuitionistic logic. In this logical system, we can make statements and + talk about their truth value. As long as we've created a series of logical + arguments from the axioms at the start to get to "true", we're all good. + Under this framework, we can talk about things without knowing what they + are, so we can prove things like "given many non-empty sets, we can choose one + item out of each set" without actually being able to name any items or a way + to pick items (see Axiom of Choice) + +- **Intuitionistic logic**, also called **constructive logic**: the new kid on + the block. In intuitionistic logic, we need to find a _witness_ for all of + our proofs. Also, falsehood is the absence of a witness, just like all the + stuff with the bottom type we just talked about, which models impossibility or + absurdity. In this logical system, the Axiom of Choice doesn't make any sense: + the act of proving that a choice exists involves generating an example of some + sort. Another notable difference is that intuitionistic does not consider the + Law of Excluded Middle to be true. + +However, intuitionistic logic is preferred in a lot of mechanized theorem +provers, because it's easier computationally to talk about "having a witness". +Let's actually look more closely at what it means to have a "witness". + +If you didn't read the section earlier about using private constructors to +restrict type construction, I'm going to revisit the idea a bit here. Consider +this very restrictive hash map: + +```ts +namespace HashMap { + class Ticket { ... } // Private to namespace + + export class HashMap { + ... + public insert(k: string, v: number): Ticket { ... } + + public getWithoutTicket(k: string): number | null { + if (!this.hasKey(k)) return null; + return this.inner[k]; + } + + public getWithTicket(t: Ticket): number { + return this.inner[t.key]; + } + } +} +``` + +The idea behind this is kind of like having a witness. Whenever you insert +something into the map, you get back a ticket that basically proves that it was +the one that inserted it for you in the first place. + +Since we used a namespace to hide access to the `Ticket` class, the only way you +could have constructed a ticket is by inserting into the map. The ticket then +serves as a _proof_ of the existence of the element inside the map (assuming you +can't remove items). + +Now that we have a proof, we don't need to have `number | null` and check at +runtime if a key was a valid key or not. As long as we have the ticket, it +_guarantees_ for us that that key exists and we can just fetch it without asking +any questions. + +In mechanized theorem provers, + +--- + +To talk about that, we have to go back to treating types as sets. For example, +we've already seen that the bottom type is a set with no elements, $\emptyset$. +But what's a type that corresponds to a set with one element? + +In type theory, we call this a **unit type**. It's only got one element in it, +so it's not super interesting. But that makes it a great return value for +functions that aren't really returning anything, but _do_ return at all, as +opposed to the bottom types. Typescript has something that behaves similarly: + +```ts +function returnUnit(): null { + return null; +} +``` + +There's nothing else that fits in this type. (I realize `void` and `undefined` +also exist and are basically single-valued types, but they have other weird +behavior that makes me not want to lump them in here) + +Let's just also jump into two-valued types, which in math we just call +$\mathbf{2}$. This type has a more common analog in programming, it's the +boolean type. + +Do you see how the number of possible values in a type starts to relate to the +_size_ of the set now? I could go on, but typically 3+ sets aren't common enough +to warrant languages providing built-in names for them. Instead, what languages +will do is offer _unions_, which allow you to create your own structures. + +For example, let's try to create a type with 3 possible values. We're going to +need 3 different unit types such that we can write something like this: + +```ts +type Three = First | Second | Third; +``` + +We can just do three different unit classes. + +```ts +class First { + static instance: First = new First(); + private constructor() {} +} +class Second { ... } // same thing +class Third { ... } // same thing +``` + +The reason I slapped on a private constructor and included a singleton +`instance` variable is to ensure that there's only one value of the type that +exists. Otherwise you could do something like this: + +```ts +let first = new First(); +let differentFirst = new First(); +``` + +and the size of the `First` type would have grown beyond just a single unit +element. + +But anyway! You could repeat this kind of formulation for any number of +_finitely_ sized types. In the biz, we would call the operator `|` a +**type-former**, since it just took three different types and created a new type +that used all three of them. [proposition]: https://en.wikipedia.org/wiki/Propositional_calculus [typescript]: https://www.typescriptlang.org/ [never]: https://www.typescriptlang.org/docs/handbook/2/functions.html#never +[false]: https://en.wikipedia.org/wiki/Principle_of_explosion +[as]: https://www.typescriptlang.org/docs/handbook/2/everyday-types.html#type-assertions +[//]: https://code.lol/post/programming/higher-kinded-types/ +[//]: https://ayazhafiz.com/articles/21/typescript-type-system-lambda-calculus