Becoming a logician with TypeScript
Tags: typescript, typetheory, logic
Published: 2019-09-17 08:34:26


Logic and computation are two sides of the same coin —this is called the **[Curry-Howard correspondence][1]**.

<video src="https://media.giphy.com/media/BmmfETghGOPrW/giphy.mp4" autoplay loop muted class="centered"></video>

## Eh?

Let's explore what this means in a short tour, by the end of which I aim to convince you that, as a developer writing TypeScript, **you are writing propositions and proofs** for a living!

Throughout recent history, computer scientists and logicians seem to keep discovering the same concepts independently —each new concept discovered in one field seems to neatly map to one in the other.

This duality has been a great driver of innovation in practical type systems — for example, the discovery of new formal logics such as [linear logic][2] led to Rust's famous borrow checker.

Let's use TypeScript to explore how everyday types, our bread and butter, acquire a new meaning when looked at from... the other side.

## Proving the obvious

Let's look at possibly the simplest type we use in our everyday job: `number`.

```typescript
const n: number = 4
```

This code typechecks —it has a type and a value that matches that type. But how does this have anything to do with formal logic?

We can look at the type `number` as a logical **proposition**, which in plain language we could express as **there exists a number**. Pretty obvious right? But TypeScript won't believe us _until we prove it_. And that proof is _the value 4_.

Let's re-read the above code as:

- The type `number` is the **proposition** or claim that _there exists a number_
- The value `4` is a valid **proof** of that proposition or claim
- TypeScript is convinced with our proof, so our program type-checks!

## This, and that too

If simple types are claims that values of that type simply exist... what are tuples?

```typescript
const nameAndAge: [string, number] = ['Curry', 119]
```

Turns out tuples let us have our cake and eat it too, that is, do conjunction! Again, let's put our logician hats:

- The tuple type `[string, number]` is the **proposition** that _there exists a string AND there exists a number_.
- The value `['Curry', 119]` is a valid **proof** of that proposition
- That is convincing enough for TypeScript, and so our program type-checks!

## What about or?

Similarily, union types let us _or_ propositions together:

```typescript
const nameOrAge: string | number = 'Curry'
```

- The union type `string | number` is the **proposition** that _there exists a string OR a number_ (a non-exclusive `or` like we're used to in programming)
- The value `'Curry'` is a valid **proof** of that proposition
- TypeScript says sure, type-checked!

## If this, then that

Probably the most interesting kind of TypeScript types from the point of view of logic are... function types!

```typescript
function add(a: number, b: number): number {
  return a + b
}
```

Functions represent **logical implication** (if `x`, then `y`). Let's see how:

- The function type `(a: number, b: number): number` is the **proposition** that _if there exists a number `a` and a number `b`, there also exists a third number_ (the return value).
- The implementation `return a + b` is a valid **proof** that you can effectively make a number given these two numbers.

### Less is more

As you've probably noticed, just as there are many numbers of type `number`, there are many implementations of the function `(a: number, b: number): number`!

One possible implementation could always return `42`, and it would still type-check, because you were able to produce a `number` given `a` and `b`, even if you didn't use them.

That is why, the more expressive a type system is, the more you can _constrain types_ (propositions), so that there are _fewer valid implementations_ (proofs) — and so that the type-checker will reject more invalid ones!

## Generalizing with... generics

> All generalizations are dangerous, even this one.
>
> _Alexandre Dumas-fils_

How do generic types come into play? What do they mean in logic? They are a way to generalize claims, so that we don't have to concern ourselves with unnecessary detail.

```typescript
function length<A>(array: Array<A>): number {
  return array.length
}
```

In formal logic, they are akin to _universal quantification_ of propositions (claiming that a proposition holds for all things, for every case). Let's look at it from the point of view of TypeScript:

- The function type `(array: Array<A>): number` is the **proposition** that _for any type `A`, if there exists an array of `A`s, there also exists a number_ (the return value, its length).
- The implementation `array.length` is a valid **proof** that you can effectively make a number given an array of absolutely any type.

## Staring at the abyss: never say `never`

In any cool formal logic, there should be a way to swear. TypeScript has the `never` type for that! Let's look at how it's used in practice.

```typescript
function goOnForever(a: number): never {
  while (true) {
    console.log('I never end!')
  }
}
```

The type `never` is also known as the bottom type, and it has **no values**. That means we can **never return anything** from this function (and I mean NOTHING, not even `undefined` or `null`). In plain English, I like to translate it as the proposition **we are screwed**.

- The function type `(a: number): never` is the **proposition** that _if there exists a number `a`, we're screwed_.
- The implementation never returns any value, and so no further reasoning can be done. We're screwed. TypeScript happily type-checks, because we did fulfill our promise: that we'll never return anything at all.

## Promising the moon

Lastly, let's look at an impossible type (proposition), and try to implement (prove) it:

```typescript
function arbitrary<A>(): A { ... }
```

What? We are claiming that _for any type A, we can come up with a value of that type_. Over-confident much? How are you going to implement that function so that you can create a value of type `number`, `Record<string, Password>`, and `UserPreferencesFactory` and whatever else I throw at this function as type `A`?

This function is surely impossible to implement... in a sound type system. But lo and behold, this type-checks:

```typescript
function arbitrary<A>(): A {
  return (null as unknown) as A
}
```

Aha! Turns out TypeScript is not sound —and neither are most modern practical type systems. That's not necessarily a bad thing, but it offers us a major way to screw up our programs. Be careful!

Ambrose Bonnaire-Sergeant wrote an [insightful piece][3] about why unsoundness in modern type systems might not be a bad thing.

## Conclusion

If you enjoyed this post and want to learn more about these ideas, I recommend you read Philip Wadler's paper [Propositions as Types][4]. It's very well-written, witty and understandable even by non-mathy types like me.

I also gave a few talks about the topic, and the potential of expressive type systems to make our programs safer (and thus, our world, increasingly dependant on those programs). Watch it [here][5].

Now I shall let you go get back to your propositions and proofs, I mean, your TypeScript project.

<small>Cover photo by Benjamin Lizardo on [Unsplash][6]</small>

[1]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence
[2]: https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf
[3]: https://blog.ambrosebs.com/2018/04/07/unsoundness-in-untyped-types.html
[4]: https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf
[5]: https://vimeo.com/191131741
[6]: https://unsplash.com/photos/IZsbWBZ08cs