Except that types are not a "new concept". The earliest programming languages already had them. To be sure, early type systems were horrible hacks and many improvements have been made, but I really don't see how knowing that "one may construct functors between the category of linear type systems and the category of closed symmetric monoidal categories" enables anyone to write code more effectively than knowing that types are (at least conceptually) subsets of data, and that some conclusions about them can be made at compile-time.
Now, I don't discount the possibility that I might be missing something, maybe even something very cool and powerful. But I have been coding for over 40 years and I have a Ph.D. in computer science, so I'm not a complete idiot. But so far no one has been able to explain to me what that thing is that I'm missing in terms that I can understand. That is what I am complaining about.
> The earliest programming languages already had them.
I'm not sure which programming language you're referring to, but as you may see in the video I posted elsewhere in this thread, the notion of computer algorithms predate transistors by a few centuries, and the notion of computability, the groundwork for types, predates transistors by a few decades.
The first people that had a stab at it were logicians, and they were used to some abstractions that probably felt as natural as code to you, while the concept of compilation wouldn't exist for another half-century.
> I have been coding for over 40 years and I have a Ph.D. in computer science, so I'm not a complete idiot. But so far no one has been able to explain to me what that thing is that I'm missing in terms that I can understand. That is what I am complaining about.
If you're looking for scientists to popularize breaking research work, you're probably barking up the wrong tree. You'll find plenty of accessible work explaining modern type systems (e.g. f# for fun and profit), it's just that this work didn't exist when scientists set about to solve this problem.
I was referring to Fortran, which distinguished between two types: floats and integers.
> The first people that had a stab at it were logicians
Yes, I know. The original article pointed that out.
> it's just that this work didn't exist when scientists set about to solve this problem.
Yes, I know that too. But it exists today and so today there isn't any reason not to avail onesself of that knowledge when engaging in pedagogy.
I have no idea what we are actually arguing about here. All my original comment was intended as was to echo the sentiment expressed in the first sentence of the original article, that's all.
Now, I don't discount the possibility that I might be missing something, maybe even something very cool and powerful. But I have been coding for over 40 years and I have a Ph.D. in computer science, so I'm not a complete idiot. But so far no one has been able to explain to me what that thing is that I'm missing in terms that I can understand. That is what I am complaining about.