From 079c2a8b381b471088331bdcb6496dff6cbf47bd Mon Sep 17 00:00:00 2001 From: Michael Zhang Date: Thu, 20 Apr 2023 15:58:15 -0500 Subject: [PATCH] Proof post --- assets/sass/_content.scss | 20 +- .../posts/2023-04-20-programmable-proofs.md | 248 ++++++++++++++++++ layouts/posts/single.html | 7 + 3 files changed, 274 insertions(+), 1 deletion(-) create mode 100644 content/posts/2023-04-20-programmable-proofs.md diff --git a/assets/sass/_content.scss b/assets/sass/_content.scss index 4ec71e9..126d000 100644 --- a/assets/sass/_content.scss +++ b/assets/sass/_content.scss @@ -289,6 +289,9 @@ details { summary { cursor: pointer; + position: sticky; + top: 0; + background-color: $background-color; } } @@ -334,6 +337,11 @@ table.table { background-color: $tag-color; padding: 2px 7px; + &.draft { + background-color: orange; + color: black; + } + .text { text-decoration: none; } @@ -456,8 +464,18 @@ table.table { details { border: 1px solid lightgray; - padding: 10px 30px; + // padding: 10px 30px; font-size: 0.9rem; + padding: 0 30px; + line-height: 1.5; + + summary { + padding: 10px 0; + } + + &[open] summary { + border-bottom: 1px solid lightgray; + } } hr { diff --git a/content/posts/2023-04-20-programmable-proofs.md b/content/posts/2023-04-20-programmable-proofs.md new file mode 100644 index 0000000..3055971 --- /dev/null +++ b/content/posts/2023-04-20-programmable-proofs.md @@ -0,0 +1,248 @@ ++++ +title = "Programmable Proofs" +date = 2023-04-20 +tags = ["type-theory"] +math = true +draft = true ++++ + +Today I'm going to convince you that data types in programming are the same as +[_propositions_][proposition] in the logical sense. Using this, we can build an +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. + +--- + +Let's start with a very simple data type: 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? + +- We can make some `Cake` like this: + + ```ts + let cake = new Cake(); + ``` + +- We can use it in function definitions, like this: + + ```ts + function giveMeCake(cake: Cake) { ... } + ``` + +- We can put it in other types, like this: + + ```ts + type Party = { cake: Cake, balloons: Balloons, ... }; + ``` + +Ok that's cool. But what about classes with no constructors? + +```ts +class NoCake { + private constructor() {} +} +``` + +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: + + ```ts + function getUsername(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. + ... + } + ``` + + 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) { + // We can just skip the first part entirely now! + // Because of the type of the input, we are sure that id is valid. + ... + } + ``` + + 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; + } + } + ``` + + 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 + 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); + } + } + ``` + + 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); + } + } + ``` + + 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 +any other static methods that would call this constructor either. That's the +full implementation of this class. We have now guaranteed that _no one can ever +create an instance of this class_. + +But what about our use cases? + +- We can no longer make `NoCake`. This produces a code visibility error: + + ```ts + let cake = new NoCake(); + ``` + + You'll get an error that reads something like this: + + > Constructor of class `NoCake` is private and only accessible within the class declaration. + +- We can no longer use it in function definitions or type constructors, like + this: + + ```ts + function giveMeCake(cake: NoCake) { ... } + type Party = { cake: NoCake, balloons: Balloons, ... }; + ``` + + Interestingly, this actually still typechecks! Why is that? + + The reason is that even though you can never actually call this function, the + _definition_ of the function is still valid. (the more technical reason behind + this has to do with the positivity of variables, but that's a discussion for a + later day) + + In fact, functions and types like this will actually be very useful for us + 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. + +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_, +but in logic and type theory we typically write it as $\bot$ and read it as +"bottom". + +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`. + +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: + +```ts +// Throw an error +function never1(): never { + throw new Error("fail"); +} + +// Infinite loop +function never2(): never { + while (true) { } +} +``` + +The reason why these are both considered `never`, or $\bot$-types, is because +imagine using this in a program: + +```ts +function usingNever() { + let canThisValueExist = never1(); + console.log(canThisValueExist); +} +``` + +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. + +[proposition]: https://en.wikipedia.org/wiki/Propositional_calculus +[typescript]: https://www.typescriptlang.org/ +[never]: https://www.typescriptlang.org/docs/handbook/2/functions.html#never diff --git a/layouts/posts/single.html b/layouts/posts/single.html index e02828f..e0ed0d5 100644 --- a/layouts/posts/single.html +++ b/layouts/posts/single.html @@ -16,6 +16,13 @@

{{ .Title }}

+ {{ if .Draft }} + + + draft + + {{ end }} + {{ range .Params.tags }}