3 ms·

Brendan Eich's bosses would be so proud that after 30 years JavaScript has finally become a true Java script. What are "reverse mapped types" called in regular

by lupire 2y ago

Brendan Eich's bosses would be so proud that after 30 years JavaScript has finally become a true Java script. What are "reverse mapped types" called in regular computer science type theory?

ivanjermakov 2y ago
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/lgwjwn5 https://www.reddit.com/r/typescript/comments/1elj65m/comment...
zarzavat 2y ago
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.
lifthrasiir 2y ago
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).
- Kinrany 2y ago
  Since there's no previous stage where compile-time expressions could be type checked, the best they can have is strong dynamic typing, no?
  - lifthrasiir 2y ago
    Not quite, because the previous stage can be dynamically generated as needed.

by lupire 2y ago

Brendan Eich's bosses would be so proud that after 30 years JavaScript has finally become a true Java script. What are "reverse mapped types" called in regular computer science type theory?

ivanjermakov 2y ago

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/lgwjwn5 https://www.reddit.com/r/typescript/comments/1elj65m/comment...

zarzavat 2y ago

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.

lifthrasiir 2y ago

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).

Kinrany 2y ago
Since there's no previous stage where compile-time expressions could be type checked, the best they can have is strong dynamic typing, no?
- lifthrasiir 2y ago
  Not quite, because the previous stage can be dynamically generated as needed.