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 alert: it's not really possible in a sound way in TypeScript. However, to fight publication bias I believe it's important to share what I tested and why it doesn't work.

The naive implementation

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

This implementation, however, doesn’t work:

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 a safeCast method; that way we'll have a property with a type referencing both type parameters.

The previous problem is now fixed:

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

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:

But a problem remains:

Again the structural nature of TypeScript is to blame for this: 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 has a simpler way to encode this notion.

Using conditional types

Could it be that if A is a subtype of B and B is a subtype of A then A is equal B?

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

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

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’s a workaround to make conditional types non distributive:

Now, the problem of union type is solved.

But there are still some cases where Equ doesn't work as expected:

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 also constitute a corner case:

With this example, we have obvious proof that if A is a subtype of B and B is a subtype of A then, A is not necessarily equal B.

Conclusion

In its version 2.8, TypeScript doesn’t let us write a sound Equ type operator. If you really want an Equ operator that works, this is 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 the 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!