michael/blog
1
0
Fork 0
Code Issues 2 Pull requests Releases Packages 1 Wiki Activity

Write some more
All checks were successful
ci/woodpecker/push/woodpecker Pipeline was successful
Details

Browse source
This commit is contained in:
Michael Zhang 2023-04-21 01:18:34 -05:00
parent 079c2a8b38
commit afaec7c0b6
Signed by: michael
GPG key ID: BDA47A31A3C8EE6B
3 changed files with 300 additions and 115 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
assets/sass/_content.scss
View file

@ -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;
}

4
assets/sass/main.scss
View file

@ -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%);

272
content/posts/2023-04-20-programmable-proofs.md
View file

@ -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,11 +58,13 @@ 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.
<details>
<summary>Why might we want to have private constructors?</summary>
@ -69,7 +74,8 @@ anymore.
it was a valid ID:
```ts
function getUsername(id: number) {
/** @throws {Error} */
function getUsername(id: number): string {
// First, check if id is even a valid id...
if (!isIdValid(id)) throw new Error("Invalid ID");
@ -83,14 +89,16 @@ anymore.
around numbers and doing the check every time.
```ts
function getUsername(id: UserId) {
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.
...
}
```
You could probably imagine what an implementation of this type looks like:
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 {
@ -115,7 +123,9 @@ anymore.
```ts
class UserId {
private id: number;
constructor(id: number) { this.id = id; }
constructor(id: number) {
this.id = id;
}
/** @throws {Error} */
fromNumberChecked() {
@ -134,7 +144,9 @@ anymore.
```ts
class UserId {
private id: number;
private constructor(id: number) { this.id = id; }
private constructor(id: number) {
this.id = id;
}
/** @throws {Error} */
fromNumberChecked() {
@ -146,11 +158,22 @@ anymore.
```
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.
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.
</details>
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<T>(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<T>(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