Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Where Do Type Systems Come From?

blog.felipe.rs

Post reply on HN
Print view View original

41–50 of 171 posts

Re: Where Do Type Systems Come From?

#41

Post by sidlls »

chroem- wrote: post #22
dungle6 wrote: post #16

Earlier quoted context omitted.

Lolwut?

He's right. The current type theory crazy is just another in a long line cargo cult programming fads. First it was pure OOP for everything, then it was pure FP for everything, and now it's types for everything. Yes they can be useful, but it's disingenuous to act like they're a cure-all. Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.

I find that a significant fraction of the bugs introduced to the code bases I've worked on that have dynamic typing are due to issues that even a rudimentary static typing system would prevent at compile time. I'm struggling to grok how a language with no type system might look. Something post-modern and Picasso-esque? To use data in a meaningful way in a program it must be possible to reason about it, and that requires that it have at least some structure.

Re: Where Do Type Systems Come From?

#42

Post by munificent »

igravious wrote: post #24
pier25 wrote: post #4

Reminded me of Gödel's incompleteness theorems. First incompleteness theorem Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F. Second incompleteness theorem For any consistent system F within which a certain amount of elementary arithmetic can be carried…

Honest question. What in the article prompted you to think about Gödel and his theorems? Why were you reminded?

I'm not sure why pier25 was reminded, but Russell's type theory and Gödel's incompleteness theorem are closely related. They both arose in response to the foundational crisis in mathematics [1].

Russell stumbled onto Russell's paradox (among others) and it shook mathematicians' confidence that everything in math was built on top of a perfectly consistent and stable foundation. If you can define a set that it "the set of sets that don't contain themself" then what other kind of crazy talk can you say in math? How do you know proven things are true and false things can't be proven in the face of weirdness like that?

Russell tried to solve the problem by inventing type theory. Types stratify the universe of values such that "the set of sets that don't contain themself" is no longer a valid statement to make.

Meanwhile, Gödel went and proved that, sorry, no, math is not consistent and complete. There are statements that are true but which cannot be proven.

[1]: https://en.wikipedia.org/wiki/Foundations_of_mathematics#Fou...

Re: Where Do Type Systems Come From?

#43

Post by naasking »

zzzcpan wrote: post #13

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming." It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with…

> It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs

Seems you don't know much about types then. I suggest you look up theorems provers and compcert and the TyPiCal language, as but a few examples.

Re: Where Do Type Systems Come From?

#44

Post by naasking »

Jtsummers wrote: post #27
zzzcpan wrote: post #13

"Even though theoretically, type theories and type systems are not enough to prevent all the problems in logic and programming, they can be improved and refined to prevent an increasingly number of problems in the practice of logic and programming." It's actually just a belief. Nothing suggests that type systems and type theories can be improved to be practical at preventing bugs. I'd say it's the opposite, even with…

What are the other approaches for preventing bugs you have in mind that are novel or increasing in application? We've done testing since the start. Still many bugs. We've done ad hoc modeling (behavior driven) for years with some improvement. Formal methods aren't popular but are successful at least at some (small to the low end of medium) scales or within portions of large scale systems. Type systems can and have be…

> We've done testing since the start. Still many bugs.

Exactly, as the OP clearly doesn't understand, but every researcher in programming languages does, test can only prove the presence of bugs, it cannot prove their absence. Types can.

Re: Where Do Type Systems Come From?

#45

Post by [deleted] »

igravious wrote: post #21
agumonkey wrote: post #5

Types are close to adjoint functors / adjunctions and partial evaluation. Assigning restricted information to part of a structure to gain knowledge through limitation (math).

The category-theory window onto the world of types only appeals to a small subset of human minds. For the average programmer you may as well be spouting gibberish because the average programmer will have no way to evaluate the claims (if any) you are making. Note, I am saying that you may as well be and not that you are . Please do not misunderstand me. Types systems certainly are formal theoretical systems but I per…

[deleted]

Re: Where Do Type Systems Come From?

#47

Post by a-nikolaev »

Watch Oregon Programming Language School lectures "Basic Proof Theory" by Frank Pfenning.

https://www.cs.uoregon.edu/research/summerschool/summer15/cu...

Very clean and easy to follow video lectures on the relation between, types, programs, and logical proofs. One does not need functors and monoids to appreciate the beauty of functional type systems. (And to see why such type systems are indeed discovered rather than invented.)

Re: Where Do Type Systems Come From?

#48

Post by incan1275 »

I share the author's frustration with wikipedia sometimes - people usually go to wikipedia for a distilled, comprehensible description of the subject matter. What he quoted was certainly not comprehensible, even to someone well-educated in CS foundations.

Re: Where Do Type Systems Come From?

#50

Post by khedoros1 »

miguelrochefort wrote: post #15

Don't they teach this stuff in school?

We danced around the edges of set theory. Symbolic logic. Combinatorial and sequential logic (especially as applies to logic circuit design). Examples of a few families of type systems, how to use them, and the practical differences between them. We didn't tend to dive deeply into the mathematical underpinnings.
Post reply on HN