3 ms·

Likewise here. After BASIC, I learned Pascal, in the early 80s. We were taught the principle that if you designed your data types right, the rest of the program

Likewise here. After BASIC, I learned Pascal, in the early 80s. We were taught the principle that if you designed your data types right, the rest of the program would practically write itself. What I can't tell you is if data types in computer programs are related to type theory.

derriz 1y ago
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.
mindcrime 1y ago
What I can't tell you is if data types in computer programs are related to type theory. I'm far from an expert on this, but my understanding is that there is some relation between the two notions. But I couldn't even begin to quantify the strength of that relation, or explain any of the details. Which is sort of what led me down this path in the first place. Some random thing I read got me thinking that deeper knowledge of type theory could be useful from an AI perspective, and that led me down the rabbit hole of looking for info on type theory. And from what I've read so far, it seems like type theory (more so than, say, set theory, or maybe even category theory) is "closer" in some sense to computer science and does in some sense relate to how types (as used in programming languages) can be constructed and reasoned about. I have a lot more to learn, needless to say. :-)

derriz 1y ago

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.

mindcrime 1y ago

What I can't tell you is if data types in computer programs are related to type theory. I'm far from an expert on this, but my understanding is that there is some relation between the two notions. But I couldn't even begin to quantify the strength of that relation, or explain any of the details. Which is sort of what led me down this path in the first place. Some random thing I read got me thinking that deeper knowledge of type theory could be useful from an AI perspective, and that led me down the rabbit hole of looking for info on type theory. And from what I've read so far, it seems like type theory (more so than, say, set theory, or maybe even category theory) is "closer" in some sense to computer science and does in some sense relate to how types (as used in programming languages) can be constructed and reasoned about. I have a lot more to learn, needless to say. :-)