x.md

In this case, it looks like TypeScript unifies the function type parameters. Flow does not unify function type parameters. Instead Flow defines “bounds” for function type parameters. Which is the more expressive choice when type-checking JavaScript.

Consider the following function:

function choose<T>(a: T, b: T): T {
  return Math.random() > 0.5 ? a : b;
}

choose(42, 'foo');

In this program, TypeScript produces two constraints. T = number and T = string. Since number does not equal string, TypeScript errors. But this is a completely valid program! In this case TypeScript limits expressivity for convenience.

Flow also produces two constraints. However, whereas TypeScript produced equality constraints (=). Flow produces subtyping constraints (<:). The constraints Flow produces are: number <: T and string <: T. Note the directionality! Since T is a supertype of both number and string we can say that number | string <: T. Effectively Flow has inferred that T is the union number | string.

Other functional programming languages like OCaml and Haskell also use unification. Unlike JavaScript, compiled languages like OCaml do not have anonymous runtime unions like JavaScript. That is you can’t express Int | String in Haskell without a data type.

Here’s the same function in OCaml (since OCaml allows side effects):

let choose : 'a -> 'a -> 'a = fun a b -> if random_bool () then a else b

let _ = choose 42 "foo"

Similar to TypeScript, OCaml produces two constraints. T = int and T = string. Since int is not a string, OCaml errors.

Now consider:

function choose<T>(a: T, b: (T) => void): T {
  b(a);
  return a;
}

choose(42, (x: string) => x.split(','));

Flow does error on this example! Since b(a) would call (42).split(',') which would be a runtime error! How does Flow decide that this is an error? Likewise, Flow produces two subtyping constraints. number <: T and T <: string. Notice that this time, number and string are not on the same side. So number “flows” through T and reaches string. Since number is not a subtype of string (number <: string is invalid), Flow errors.

This is where variance comes in to play. Inputs always add a lower bound to type variables (number <: T), but inputs of inputs flip and add an upper bound to type variables (T <: string).

Going back to ===, consider:

function strictEqual<T>(a: T, b: T): boolean {
  return a === b;
}

42 === 'foo';
strictEqual(42, 'foo');

TypeScript errors on both cases thanks to unification. Flow errors on neither case thanks to subtyping.

If Flow errored on 42 === 'foo', but not strictEqual(42, 'foo') that would be unsound! (Although erroring on 42 === 'foo' would be a good candidate for a lint rule. Lint rules are free to produce warnings for cases that aren’t technically runtime errors, but are likely logic errors.)

So TypeScript makes this choice for convenience. However, while this choice is not in itself unsound, it makes common JavaScript patterns like classes completely useless without some sacrifies to soundness. This decision betrays the fundamental unsoundness in TypeScript.

Ever wonder why function programming languages don’t have classes with inheritance? Or why object oriented languages don’t have inference of the same power as functional programming languages? Consider:

class Animal {}
class Cat extends Animal {}
class Dog extends Animal {}

Animal is a subtype of Cat (Cat <: Animal), but Cat is not a subtype of Animal (Animal <: Cat is invalid)! This means Cat != Animal. For two types to be equal (T = U), both types must be subtypes of each other (T <: U and U <: T).

Now consider:

function pet(x: Animal) {}

pet(new Cat());

This passes TypeScript. But if TypeScript used sound unification this should not pass TypeScript. TypeScript tries to check Cat = Animal. This fails, so then TypeScript checks both Cat <: Animal and Animal <: Cat. Since the former passes, TypeScript does not complain.

To demonstrate how this leads to invalid program construction, consider:

function pet(a: Animal, b: (x: Animal) => void) {
  b(a);
  return a;
}

pet(new Dog(), (x: Cat) => {});

TypeScript accepts this program.

Why? Well first TypeScript checks Animal = Dog. This fails. So then TypeScript checks Dog <: Animal and Animal <: Dog. The former passes and the latter fails. So TypeScript considers the first argument ok.

Then TypeScript checks Animal = Cat. This fails. So then TypeScript checks Cat <: Animal and Animal <: Cat. The former passes and the latter fails. So TypeScript considers the second argument ok.

This example fails Flow. Because Flow performs proper subtype checking. Flow checks Dog <: Animal which passes. Then Flow checks Animal <: Cat which fails. So Flow reports an error.

In trying to be convenient, TypeScript sacrifies soundness. It tries to unify and then tries to subtype. You can’t do both and also be sound.