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

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 As, 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.

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