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

Use Your Type System

dzombak.com

Post reply on HN
Print view View original

241–250 of 357 posts

Re: Use Your Type System

#241

Post by ChadNauseam »

scottgg wrote: post #109
josephg wrote: post #25

Earlier quoted context omitted.

Yep. For this reason, I wish more languages supported bound integers. Eg, rather than saying x: u32, I want to be able to use the type system to constrain x to the range of [0, 10). This would allow for some nice properties. It would also enable a bunch of small optimisations in our languages that we can't have today. Eg, I could make an integer that must fall within my array bounds. Then I don't need to do bounds ch…

The generic magic for this is called “dependant types” I believe - generics that can take values as well as types as parameters. Idris supports these

What the GP described could be achieved with dependent types, but could also be achieved with a less powerful type system, and the reduced power can sometimes lead to enormous benefits in terms of how pleasant it actually is to use. Check out "refinement types" (implemented in Liquid Haskell for example). Many constraints can be encoded in the type system, and an SMT solver runs at compile time to check if these constrains are guaranteed to be satisfied by your code. The result is that you can start with a number that's known to be in [0..10), then double it and add five, and then you can pass that to a function that expects a number in [10..20). Dependent types would typically require some annoying boilerplate to prove that your argument to the function would fall within that range, but an SMT solver can chew through that without any problem.

Re: Use Your Type System

#242

Post by bern4444 »

This seems like a conclusion derived from the ideas in parse don't validate[1].

The goal is to encode the information you learn while parsing your data into your type system. This unlocks so many capabilities: better error handling, making illegal states unrepresentable, better compiler checking, better autocompletion etc.

[1]https://lexi-lambda.github.io/blog/2019/11/05/parse-don-t-va...

Re: Use Your Type System

#243

Post by jhhh »

The problem with this post is that the author is conflating two different things. Using a type system to capture the units of a measurement or metric is straightforwardly better than having them be implied. Stripping a numeric value and unit down to just a value involves an obvious loss of information. That situation is wholly different than just wrapping your UUID in some bespoke type which doesn't provide any extra information. They just look the same because you're mechanically doing something similar (ie. wrapping some primitive or standard type in something else). Not to mention unless you want to make your wrappers monads you're going to have to unwrap them at some point anyway at which point you can still transpose the actual type when you have to call any external library/function. I would love to know what the test suites of these 'many bugs in real systems' projects looked like. I suspect the test suite coverage wasn't very good.

Re: Use Your Type System

#244

Post by rmunn »

dajonker wrote: post #193
MantisShrimp90 wrote: post #40

Im on the opposite extreme here in that I believe typing obsession is the root of much of our problems as an industry. I think Rich Hickey was completely right, this is all information and we just need to get better at managing information like we are supposed to. The downside of this approach is that these systems are tremendously brittle as changing requirements make you comfort your original data model to fit the…

A lot of us programmer folk are indefinitely in search of that one thing that will finally let us write the perfect, bug-free, high performance software. We take these concepts to the extreme and convince ourselves that it will absolutely work as long as we strictly do it the Right Way and only the Right Way. Then we try to convince to our fellow programmers that the Right Way will solve all of our problems and that…

A wise person once told me that if you ever find yourself saying "if only everyone would just do X...", then you should stop right there. Never, ever, in the history of the world has everyone done X. No matter how good an idea X is, there will always be some people who say "No, I'm going to do Y instead." Maybe they're stupid, maybe they're evil, maybe they're just ignorant... or maybe, just maybe, X was not the best thing for their particular needs and Y was actually better for them.

This is an important concept to keep in mind. It applies to programming, it applies to politics, it applies to nearly every situation you can think of. Any time you find yourself wishing that everyone would just do X and the world would be a better place, realize that that is never going to happen, and that some people will choose to do Y — and some of them will even be right to do so, because you do not (and cannot) know the specific needs of every human being on the planet, so X will not actually be right for some of them.

Re: Use Your Type System

#245

Post by Jtsummers »

bigstrat2003 wrote: post #234
Jtsummers wrote: post #50

Earlier quoted context omitted.

Setting aside the objections some have to exceptions generally: Checked exceptions, in contrast to unchecked, means that if a function/method deep in your call stack is changed to throw an exception, you may have to change many function (to at least denote that they will throw that exception or some exception) between the handler and the thrower. It's an objection to the ergonomics around modifying systems. Think of…

> Checked exceptions, in contrast to unchecked, means that if a function/method deep in your call stack is changed to throw an exception, you may have to change many function (to at least denote that they will throw that exception or some exception) between the handler and the thrower. That's the point ! The whole reason for checked exceptions is to gain the benefit of knowing if a function starts throwing an excepti…

Why are you screaming? All those wasted exclamation marks, you could have written something I didn't know. I didn't say it wasn't the point or that it was a bad thing.

Re: Use Your Type System

#246

Post by SAI_Peregrinus »

9rx wrote: post #173
munificent wrote: post #149

Earlier quoted context omitted.

> Even in an OOP language you probably want `UUID.from(string): Maybe `, not `new UUID(string)` that throws. One way to think about exceptions is that they are a pattern matching feature that privileges one arm of the sum type with regards to control flow and the type system (with both pros and cons to that choice). In that sense, every constructor is `UUID.from(string): MaybeWithThrownNone `.

The best way to think about exceptions is to consider the term literally (as in: unusual; not typical) while remembering that programmers have an incredibly overinflated sense of ability. In other words, exceptions are for cases where the programmer screwed up. While programmers screwing up isn't unusual at all, programmers like to think that they don't make mistakes, and thus in their eye it is unusual. That is what…

Unfortunately many languages treat exceptions as a primary control flow mechanism. That's part of why Rust calls its exceptions "panics" and provides the "panic=abort" compile-time option which aborts the program instead of unwinding the stack with the possibility of catching the unwind. As a library author you can never guarantee that `catch_unwind` will ever get used, so its main purpose of preventing unwinding across an FFI boundary is all it tends to get used for.

Re: Use Your Type System

#247

Post by folkrav »

johnfn wrote: post #213
folkrav wrote: post #167

Earlier quoted context omitted.

It would be weak if that was actually mutating the first “a”. That second declaration creates a new variable using the existing name “a”. Rust lets you do the same[1]. [1] https://doc.rust-lang.org/book/ch03-01-variables-and-mutabil...

Rust lets you do the same because the static typing keeps you safe. In Rust, treating the second 'a' like a number would be an error. In ruby, it would crash.

Let’s rephrase: is naming a variable typing? As for runtime vs. compile errors - isn’t this just a trade off of interpreted languages?

Re: Use Your Type System

#248

Post by 9rx »

SAI_Peregrinus wrote: post #246
9rx wrote: post #173

Earlier quoted context omitted.

The best way to think about exceptions is to consider the term literally (as in: unusual; not typical) while remembering that programmers have an incredibly overinflated sense of ability. In other words, exceptions are for cases where the programmer screwed up. While programmers screwing up isn't unusual at all, programmers like to think that they don't make mistakes, and thus in their eye it is unusual. That is what…

Unfortunately many languages treat exceptions as a primary control flow mechanism. That's part of why Rust calls its exceptions "panics" and provides the "panic=abort" compile-time option which aborts the program instead of unwinding the stack with the possibility of catching the unwind. As a library author you can never guarantee that `catch_unwind` will ever get used, so its main purpose of preventing unwinding acr…

> Unfortunately many languages

Just Java (and Javascript by extension, as it was trying to copy Java at the time), really. You do have a point that Java programmers have infected other languages with their bad habits. For example, Ruby was staunchly in the "return errors as values and leave exception handling for exceptions" before Rails started attracting Java developers, but these days all bets are off. But the "purists" don't advocate for it.

Re: Use Your Type System

#249

Post by voidhorse »

tylerhou wrote: post #176
mcculley wrote: post #55

Earlier quoted context omitted.

Ada has this ability to define ranges for subtypes. I wish language designers would look at Ada more often.

Academic language designers do! But it takes a while for academic features to trickle down to practical languages—especially because expressive-enough refinement typing on even the integers leads to an undecidable theory.

Eh, idk.

I think the reasons are predominantly social, not theoretical.

For every engineer out there that gets excited when I say the words "refinement types" there are twenty that either give me a blank stare or scoff at the thought, since they a priori consider any idea that isn't already in their favorite (primitivistic) language either too complicated or too useless.

Then they go and reinvent it as a static analysis layer on top of the language and give it their own name and pat themselves on the back for "inventing" such a great check. They don't read computer science papers.

Re: Use Your Type System

#250

Post by vips7L »

bcrosby95 wrote: post #63
abraxas wrote: post #37

An adjacent point is to use checked exceptions and to handle them appropriate to their type. I don't get why Java checked exceptions were so maligned. They saved me so many headaches on a project where I forced their use as I was the tech lead for it. Everyone hated me for a while because it forced them to deal with more than just the happy path but they loved it once they got in the rhythm of thinking about all the…

I think most complaints about checked exceptions in Java ultimately boil down to how verbose handling exceptions in Java is. Everytime the language forces you to handle an exception when you don't really need to makes you hate it a bit more. First, the library author cannot reasonably define what is and isn't a checked exception in their public API. That really is up to the decision of the client. This wouldn't be su…

That’s the same conclusion I’ve come too. I’ve commented on it a little bit here:

https://news.ycombinator.com/item?id=44551088

https://news.ycombinator.com/item?id=44432640

> Your code probably shouldn't be throwing IOExceptions. But Java makes converting exceptions unnecessarily verbose

The problem just compounds too. People start checking things that they can’t handle from the functions they’re calling. The callers upstream can’t possibly handle an error from the code you’re calling, they have no idea why it’s being called.

I also hate IOException. It’s so extremely unspecific. It’s the worst way to do exceptions. Did the entire disk die or was the file not just found or do I not have permissions to write to it? IOException has no meaning.

Part of me secretly hopes Swift takes over because I really like its error handling.

Post reply on HN