This doesn’t seem correct.. Church was using types to delimit his lambda calculus in the 1930-40s. We had dependent type theory from Martin Lof around the same time ML was implemented! If my memory serves the calculus of constructions (the bedrock for Coq’s metatheory) was proposed around this time as well.
In fact, ML was created as part of a theorem proving system which is a fairly advanced application of type theory. We even knew that types weren’t sets thanks to Reynold’s (it turns out this model doesn’t work with polymorphism + functions, you need domains to do it properly) in the 80s.
Type theory dates well before anything implemented a fancy type system.
Indeed. While this may be a valid history of the notion of types in programming languages, it is not a history of the mathematical notion of types, which were first developed by Bertrand Russell in an attempt to construct an alternative to naïve set theory that avoids Russell’s Paradox.
Apparently, Wikipedia has a page on the History of type theory, which would be a better rendering of the broader history of types outside of programming.
This doesn’t seem correct.. Church was using types to delimit his lambda calculus in the 1930-40s. We had dependent type theory from Martin Lof around the same time ML was implemented! If my memory serves the calculus of constructions (the bedrock for Coq’s metatheory) was proposed around this time as well.
In fact, ML was created as part of a theorem proving system which is a fairly advanced application of type theory. We even knew that types weren’t sets thanks to Reynold’s (it turns out this model doesn’t work with polymorphism + functions, you need domains to do it properly) in the 80s.
Type theory dates well before anything implemented a fancy type system.
Indeed. While this may be a valid history of the notion of types in programming languages, it is not a history of the mathematical notion of types, which were first developed by Bertrand Russell in an attempt to construct an alternative to naïve set theory that avoids Russell’s Paradox.
Apparently, Wikipedia has a page on the History of type theory, which would be a better rendering of the broader history of types outside of programming.