Yeah I think there’s some confusion here. When I hear “type theory” - I think Martin-Löf, Girard’s Proofs and Types, Curry-Howard, etc. Which is not a “theory

Yeah I think there’s some confusion here. When I hear “type theory” - I think Martin-Löf, Girard’s Proofs and Types, Curry-Howard, etc. Which is not a “theory of programming language types” - although the subjects are not completely isolated from each other. Then again, it’s been decades since I actually studied this stuff and haven’t really followed either subject since. As far as the latter is concerned (programming language type systems), as an engineer, I’ve seen nothing in mainstream programming languages that advances the state-of-the-art compared to what was known back in the 1980s - when Hindley-Milner became mainstream and Luca Cardelli wrote the seminal survey papers on the subject.