Some context on the term:

> This is the lingo used in the compiler's source code, in the PRs and in the issues on GitHub.

> When you have to infer the T from a MappedType<T>, you are inverting the action of the MappedType. There is a dedicated part in the compiler for doing that.

Source: https://www.reddit.com/r/typescript/comments/1elj65m/comment...

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.

An inverse function.

While technically used like types, TypeScript "types" are really compile-time values that happen to be also usable for constraining usual run-time values like types. These compile-time values themselves do not have much types, so you can easily get errors from compile-time evaluations (which is different from compile-time type errors!). Likewise, most TypeScript type-level constructs are really long-winded methods to do the compile-time computation and have no straightforward equivalents in type systems that do guarantee the soundness and coherence (which have specific definitions).

Since there's no previous stage where compile-time expressions could be type checked, the best they can have is strong dynamic typing, no?

Not quite, because the previous stage can be dynamically generated as needed.