blog.md

Proving that two types are equal in TypeScript

All examples were tested against TypeScript 2.8.3 with strictNullChecks and strictFunctionTypes turned on.

The original intent of this article was to explain how we can write a type Equ<A, B> that proves that A and B are equal. Spoiler: it's not really possible in a sound way in TypeScript. But to fight the publication bias, I think it's important to share what I tested and why it doesn't work.

The naive implementation

In other languages, Equ is often build with a type Equ<A, B> and one (and only one) constructor named Refl<A> that extends Equ<A, B>. In TypeScript, it could be:

https://gist.github.com/f148bd6cbc2da71d22f124d3906d3a29

But this doesn't work:

https://gist.github.com/d20fa189800934d1318f24391aa82cec

This is due to the structural nature of TypeScript. Having no concrete properties, the definition of Equ is in fact completely equivalent to {}.

The less naive implementation

Equ<A, B> is generally used to cast safely A to B. Let's add this method, that way we'll have a property with a type referencing both type parameters.

https://gist.github.com/f4307bdb8737ec7e3810ce2a5ec48de7

The previous problem is now fixed:

https://gist.github.com/02338b634c6152b11980ce079979a1e2

Sadly, there is way to make it compile without using Refl:

https://gist.github.com/0809e0657203b78cf0f14af3348599df

Again, it's the structural nature of TypeScript that bites us. If someone is to make an instance of Equ, we want him to use Refl!

Fighting the structural nature of TypeScript

In TypeScript, two private properties are compatible only if they originate from the same type. We will abuse this to make the use of Refl mandatory:

https://gist.github.com/168a76aecb6cad1e94a9fc0a1d99686d

But there is still a problem:

https://gist.github.com/330643c07173e529ad387d38a91ec9b3

Again the structural nature of TypeScript is responsible: comparing Equ<A, B> and Equ<C, C> (the supertype of Refl<C>) is equivalent to comparing the signature of safeCast, ie: are A => B and C => C compatible? With the strictFunctionTypes option, C is required to be a subtype of B and a supertype of A.

Because we fix the value of C to A, in the end, our Equ<A, B> implementation only tests that A is a subtype of B.

We could then add another method safeCast2(b: B): A to workaround the problem, but in the end, it would mean A is a subtype of B and B is a subtype of A. And TypeScript have a simpler way to encode this notion.

Using conditional types

Maybe we can do a hypothesis: if A is a subtype of B and B is a subtype of A, is A equal B?

With the conditional types of TypeScript 2.8, we can try to implement this hypothesis:

https://gist.github.com/597a0b5e4d36948a15dc5d78f27b9f45

We can show right away that this doesn't work:

https://gist.github.com/c6f838f20f1b85ed8587985e1e50d239

This is due to the distributive property of the conditional type, in our case Equ<A, A | C> is distributed and is equivalent to: A extends A | C ? (C extends A ? {} : never | A extends A ? {} : never) which reduces to A extends A | C ? ({} | never) : never and {} | never is equal to {}.

Using non-distributive conditional types

There is workaround to make conditional types non distributives:

https://gist.github.com/71fb48a8d948c51c10d9ee84ff811282

Now, the problem of union type is solved.

https://gist.github.com/ae48f5abe7d7834cebe6ebfacc5fa754

But there is still some cases were Equ doesn't work as expected:

https://gist.github.com/a68a36922f47faa97dc4847fd69d55da

The way enums are implemented is unsound: any enum (E here) is a subtype of number (which is normal), but number is also a subtype of any enum (E);

null and undefined are also corner case:

https://gist.github.com/81d2b1738fe5085727c3b315359e3829

With this example, we have an obvious proof that A is subtype of B and B is subtype of A doesn't mean that A is equal B.

Conclusion

In it's version 2.8, TypeScript doesn't let us write a sound Equ type operator. If you really want an Equ operator that works, it still doable by restricting yourself to a subset of TypeScript:

• activate strictNullChecks and strictFunctionTypes
• don't use any.
• don't use enum.
• don't use null or undefined

Hoping that the specification of TypeScript is up to date, if you do that, we can now prove (with a pen and a paper, but this margin is too narrow to contain the proof) that if A is a subtype of B and B a subtype of A, then A is B.

With this we will then be able (maybe in a future article) to prove very interesting properties in TypeScript, like 1 + 2 = 3 or even n + 0 = n!