Thread by @javierwchavarri

One of the most useful ways to categorize type systems is:

- is it Hindley-Milner based? (Rust, Haskell, OCaml)
- or does it support implicit subtyping (TypeScript, Flow, C#)?

The first: 1 expression <-> at most 1 type.
The second: 1 expression <-> multiple types.

A thread 👇

Implicit subtyping works well for languages that have support for inheritance, and that's why (I guess) it made sense for Flow and TypeScript to adopt it, as JavaScript has prototype inheritance.

But implicit subtyping has trade-offs too:

Hindley-Milner type systems (HMTS) can infer very accurate types, thanks to the "1 expression <-> at most 1 type" restriction. Implicit subtyping type systems (ISTS) inference engines can’t make the same kind of assumptions.

Let's take this example:

const foo = () => Math.random() > 0.5 ? “bar” : 2;

In an ISTS, it's valid and the inferred returned type would be `string | number`.

In a HMTS, it would return a type error, as one branch has type `string` and the other `number`: they can’t be unified.

ISTS inference is expansive: every new conditional branch adds new types to the returned expression.

HMTS inference is restrictive: all conditional branches need to be "unifiable" into the same type.

What are the consequences?

ISTS inference engines are more complex, due to their expansive nature and the more relaxed constraints. So they generally require more actions from developers in the form of manually-written type annotations to compensate in part from that relaxation.

The quality of types decrease over time because:

1. we’re humans, and inferring types is a task better suited for machines (like compiling source code to assembly code)

2. our attention is now spread between writing code and inferring / writing types.

The human involvement caused by these compulsory manual type annotations has linear costs over the evolution of a project. These linear costs decrease (imo) the benefit-cost ratio of type systems in the ISTS case.

While HMTS has limitations too, at least type inference and annotations are One Less Thing I Need To Care About™️.

Plus, one can always use type annotations if needed (note that some features of HMTS-based languages might still require explicit annotations).

The whole point of this thread is to surface the fundamental differences between ISTS and HMTS.

Before you give up on type systems, make sure you have meaningfully tried at least one in both categories! The developer experience is dramatically different.

Fin.

Some resources, for those curious:

- "Subtyping is overrated", by @calebmer: (highly recommended!)
- waleedkhan.name/blog/union-vs-… by @arxanas
- codecommit.com/blog/scala/wha… by @djspiewak
- stackoverflow.com/questions/7234… (see quote by Scala's creator Martin Odersky)