Hacker News new | ask | show | jobs
by alxmng 1183 days ago
The purpose of a type system is to ensure the correctness of programs. That's what they are, that's why they were invented, that's why they were studied. That CS involves math doesn't change the fact that it's about programming.

The whole reason we want to prove a type system sound is so we can prove certain things about the programs that use that type system.
3 comments
joshuamorton 1183 days ago
That's one use, yes, but it isn't the only use. And it's certainly not why they were invented

Typed lambda calculus was formalized before the first programmable computers, and it's relation to programming wasn't clarified for another 20+ years (and real type systems don't really start to appear in programming languages for another decade after that afaik).

link
dcow 1183 days ago
You need to learn some history. Or at least cite your claims.

We use type systems to help abstract patterns of data into logical constructs that can be reasoned about. They are logic systems with grammar that describes relationships between axioms and constructs.

Seriously, go read a textbook and then we can pick this discussion up. Wikipedia has a good overview.

https://en.m.wikipedia.org/wiki/Type_theory

link
alxmng 1183 days ago
Ah, yes. Type theory originates before programming. Type theory only has relevance to computers insofar as it’s used to prove things about programs. Type theory in the context of computing is about programming.

We don’t call set theory and category theory “computer science” unless it’s about programming computers.

link
joshuamorton 1183 days ago
No, I mean that's an application yes, but I'd still call Alonzo Church a computer scientist and his work theoretical computer science.

Much as how people who study computability are computer scientist, even though none of the asymptomatic improvements to matrix multiplication since 1990 are even remotely relevant to any kind of real-life program.

link
Koshkin 1183 days ago
This is a narrow view on types; for example, types also help the compiler to produce optimized code. In general, they assist reasoning about and understanding the program.
link