We're not using "type theory" the same way, I think. I'm thinking in terms of
- simply typed lambda calculus
- System F
- dependent type theory (MLTT)
- linear types
- row types
- and so on
But it's subtle to talk about. It's not like there is a single type theory that underlies Typescript or Rust, either. These practical languages have partial, (and somewhat post-hoc) formalizations of their systems.
alt Hacker News
We're not using "type theory" the same way, I think. I'm thinking in terms of
But it's subtle to talk about. It's not like there is a single type theory that underlies Typescript or Rust, either. These practical languages have partial, (and somewhat post-hoc) formalizations of their systems.