Type System Design

A union says a value is one of several types. That is only useful if the checker can find out *which* one — so the real subject of this lesson is narrowing, and the discriminant that makes narrowing possible.

`A & B` is a value that satisfies both constraints at once. It is the right tool for mixins and for refining an over-broad type, and it will cheerfully let you write a type that no value can ever have.

Products hold several things at once; sums hold exactly one of several things. The word "algebraic" is literal — cardinalities multiply for products and add for sums — and that arithmetic is the fastest way to tell whether a data model can represent states that must never exist.

Matching is the elimination form for a sum type: it inspects the tag and binds the payload in one construct. Destructuring, guards, nested patterns and bindings are the surface; the decision tree the compiler builds from it is a separate subject.

The compiler proves that every variant is handled, and reports a concrete value if one is not. This is the payoff that makes sum types worth having — and the reason adding a variant is a breaking change.

Two ways to represent absence: a type that silently includes an extra value and a flow analysis to exclude it, or an ordinary sum type with no special status at all. They differ in what they cost you at the boundary, in the signature, and in bytes.

Static and dynamic typing in one program, with a dynamic type that is compatible with everything. The honest version of the story includes what `any` costs, why TypeScript checks nothing at runtime, and why the sound alternative has a performance problem nobody has fully solved.