TypeScript has a very different set of axiomatic operations than conventional type theory. It incorporates concepts from set theory, you have unions T|U, inter

TypeScript has a very different set of axiomatic operations than conventional type theory. It incorporates concepts from set theory, you have unions T|U, intersections T&U, comprehensions { [T in U]: e(T) }, conditionals (T extends U ? A : B ), pattern matching (infer T), and the typeof operator is like a poor man’s dependent typing. While you could certainly express all of these concepts in a language with dependent types, you can’t emulate the inference rules (the subject of TFA), so it can be said that TypeScript’s type theory is unique.