Logic and computation are two sides of the same coin βthis is called the **Curry-Howard correspondence**.

## 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 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`

.

```
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?

```
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:

```
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!

```
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*(the return value).`a`

and a number`b`

, there also exists a third number - 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.

```
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*(the return value, its length).`A`

, if there exists an array of`A`

s, there also exists a number - 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.

```
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:

```
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:

```
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 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. 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.

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

Cover photo by Benjamin Lizardo on Unsplash

## Top comments (0)