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

31–40 of 171 posts

Re: Where Do Type Systems Come From?

#31

Post by agumonkey »

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…

Do not worry I understand 99% of your message. It's indeed a land far far away from the everyday coding of the majority of programmers. Unless they start digging, which I did. If you take code as data (lisp roots showing) you start to want to reason about it and quickly you end up reading about FP, denotations, different forms of evaluations, the value of metadata (type or else).

Now I believe there's an artificial split between math leaning people and pragmatics, the former end up as PhD, the latter in IT or close. But in reality the average coder could understand and even enjoy the land of abstractions, it's just that the river he swims in isn't flowing there so one has to run against the flow.

Not to say that ideals are the only-tru-way.

Re: Where Do Type Systems Come From?

#32

Post by Retra »

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…

I guess you're just ignoring the fact that every single programming language in use today has some kind of type system? Are you clamoring for processors that don't even bother to distinguish between register sizes?

Type systems are a necessary part of computing. One can even define computing in terms of how types are transformed. Types are an extremely primitive and fundamental description of how computation happens, and without them, it'd be hard to imagine how anything could be computed at all, let alone correctly.

Re: Where Do Type Systems Come From?

#33

Post by [deleted] »

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?

[deleted]

Re: Where Do Type Systems Come From?

#34

Post by Anderkent »

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.

> Most bugs aren't type related, and you're adding additional mental overhead with these extremely elaborate type systems.

Are you? usually I find it to be the reverse - you're leveraging the type system to track some properties for you, so that you don't have to track them mentally. I.e. less mental overhead (though possibly more boilerplate-overhead)

Re: Where Do Type Systems Come From?

#35

Post by CraneWorm »

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.

For me, the elaborateness of the type system and it's checker REMOVE the overhead. YMMV, obviously.

Re: Where Do Type Systems Come From?

#36

Post by Jtsummers »

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?

Probably this part from the article:

> Similarly, type theory wasn’t enough to describe new foundations for mathematics from which all mathematical truths could in principle be proven using symbolic logic. It wasn’t enough because this goal in its full extent is unattainable.

Re: Where Do Type Systems Come From?

#37

Post by dpratt71 »

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.

What is "he" right about, exactly? You say "yes they can be useful", but that's not the impression I get from OP. I am also confused because the very quote OP is responding to states that "...type systems are not enough to prevent all the problems in logic and programming...". Do you consider that acting like type systems are a cure-all?

Re: Where Do Type Systems Come From?

#38

Post by currymj »

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.

There’s the technical aspects of the fact that every language has to have some notion of “type”. And seemingly interpreted languages might be JIT-compiled etc. This is of interest if you care about the implementation of languages.

Then there’s the opinions that users of languages with more elaborate, expressive type systems have, like how some people really enjoy Haskell or Elm because they feel that the type system helps them express their ideas clearly, avoid errors, and aids refactoring and maintenance.

If you’re worried about this one, don’t I guess? If you can use dynamic languages to achieve your goals, and you like them, then that’s fine! There are plenty of languages you can play with if you want to get a feel for programming with types. Even Java 8 and C++11 are decent at this point (I’m sure a Haskell programmer is fuming right now).

Then there’s like, a few thousand people in the world who have well-informed opinions on research into the theory of programming languages, the Curry-Howard correspondence between types and proofs. Also a lot of Hacker News posters who have heard these words. Some of them pretend like they know what they’re talking about.

Re: Where Do Type Systems Come From?

#39

Post by igravious »

agumonkey wrote: post #31
igravious wrote: post #21

Earlier quoted context omitted.

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…

Do not worry I understand 99% of your message. It's indeed a land far far away from the everyday coding of the majority of programmers. Unless they start digging, which I did. If you take code as data (lisp roots showing) you start to want to reason about it and quickly you end up reading about FP, denotations, different forms of evaluations, the value of metadata (type or else). Now I believe there's an artificial s…

I am delighted you responded so positively to what I wrote and didn't take what I wrote negatively which you could easily have done.

Let's for arguments sake say that there are two camps (broadly speaking), the pragmatists as you say and the theorists/idealists let's call them. It reminds me of the difference between someone like Torvalds and someone like Stallman.

Thing is we need both! You're right, the split _is_ artificial. The Linux kernel couldn't wait for someone to come along and create a type-awesome version of C. I mean, Rust seems to be the first attempt to take what type theorists have learned and apply it to a systems programming language. In the meantime software needs to be written and we have the tools we have.

If the fruits of type theory are going to filter through into software development I'm not sure it should come laden down with category theory (as awesome as that is) or the lambda calculus (as mind-bending as that is). I could of course be dead wrong.

Re: Where Do Type Systems Come From?

#40

Post by stepik777 »

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?

There is an official book which is very well written. I remember that I started to read it several years ago and was surprised that I actually can understand most of the things.
Post reply on HN