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

11–20 of 171 posts

Re: Where Do Type Systems Come From?

#11

Post by Drup »

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

I believe you get an actual interest for type systems when you start using a rich one. Unfortunately, most mainstream languages have very poor type systems. In particular, it will come naturally over time if you start using languages like OCaml, F#, Scala, Rust, Haskell, ...

Re: Where Do Type Systems Come From?

#13

Post by zzzcpan »

"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 as much understanding about the nature of bugs as we have today, they don't look very promising, unlikely to make it even into the top ten of other different approaches.

Re: Where Do Type Systems Come From?

#14

Post by miguelrochefort »

agumonkey wrote: post #3
smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

To each his own path. Maybe you'll change course, maybe not, maybe type theory will evolve (HoTT comes to mind).

I can't seem to grasp HoTT.

Are there any approachable resources on the subject?

Re: Where Do Type Systems Come From?

#16

Post by dungle6 »

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…

Lolwut?

Re: Where Do Type Systems Come From?

#17

Post by [deleted] »

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…

[deleted]

Re: Where Do Type Systems Come From?

#18

Post by hinkley »

smcl wrote: post #2

I feel kinda alone on HN, Lobste.rs and LtU in not having in-depth knowledge or opinions on type systems. I get that these underpin the technology we as programmers use every single day, but I'm a little ashamed that I can't get excited about the subject and feel like it's too late for me to bother trying.

I learned set theory and discrete math from this guy:

http://internethalloffame.org/about/advisory-board/cl-liu

Easily my second favorite instructor, possibly my favorite. I felt pretty prepared to deal with analysis and design in statically typed languages just from that grounding in set theory and logic. Fond of saying things like, "We have a box. What's inside that box? Another box. What's inside that box? We don't care."

Now retired, he was an early proponent of distance learning, so surely some of his stuff is accessible still.

Re: Where Do Type Systems Come From?

#19

Post by agumonkey »

miguelrochefort wrote: post #14
agumonkey wrote: post #3

Earlier quoted context omitted.

To each his own path. Maybe you'll change course, maybe not, maybe type theory will evolve (HoTT comes to mind).

I can't seem to grasp HoTT. Are there any approachable resources on the subject?

I only read two pages on homotopy so far, I cannot answer that :)

Re: Where Do Type Systems Come From?

#20

Post by dpratt71 »

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 could be at least argued that type systems aren't very effective at reducing meaningful bugs and/or aren't worth the costs they impose, but you went way beyond that argument. As I see it, the only way you can believe that "nothing suggests that type systems...can be improved to be practical at preventing bugs" is because you have willfully ignored or completely discounted every bit of evidence you've encountered that suggests otherwise.
Post reply on HN