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

21–30 of 171 posts

Re: Where Do Type Systems Come From?

#21

Post by igravious »

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 personally have come to believe that the majority of coders are ill-served by the mathematical leanings of type theorists.

I'm not sure I can explain myself better than that at the moment.

Re: Where Do Type Systems Come From?

#22

Post by chroem- »

dungle6 wrote: post #16
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?

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.

Re: Where Do Type Systems Come From?

#23

Post by alimw »

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?

Have you tried reading the articles linked to on this page? http://www.bris.ac.uk/arts/research/projects/homotopy-type-t...

Re: Where Do Type Systems Come From?

#24

Post by igravious »

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?

Re: Where Do Type Systems Come From?

#26

Post by kazinator »

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…

Type theorists are people who understand arrows very well -- as long as those arrows aren't pointers. :)

Re: Where Do Type Systems Come From?

#27

Post by Jtsummers »

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 been used for codifying concepts from all of these into the program semantics. So I'm not sure how it is that they don't help.

Re: Where Do Type Systems Come From?

#28

Post by swsieber »

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…

There are type systems that prevent race issues, use after free, and null pointer exceptions.

So saying that they aren't practical at solving bugs is a little disingenuous.

Re: Where Do Type Systems Come From?

#29

Post by Jtsummers »

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.

Types aren't new. As the article discusses they date back over a century at least in math and logic. Within programming, we've had them in every major language for decades. The first big push for strong and expressive type systems is from the functional programming work which led to the ML family and the work that made Pascal and Ada on the imperative (and later OO variants) side, which dates back some 40-50 years now.

Re: Where Do Type Systems Come From?

#30

Post by 0xCMP »

miguelrochefort wrote: post #15

Don't they teach this stuff in school?

The school I went to barely taught C/C++ and the absolute minimum of PHP, CSS, Linked Lists, and Hash Maps. Very sad that so many actually smart people can't graduate knowing much just doing their course work. Let alone imagine those who lack off a bit and still pass. Unless you're programming on your own, like I was along with a few others, you graduate possibly in debt and completely unprepared.

So no, they never get in to this stuff.

Post reply on HN