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

181–190 of 357 posts

Re: Use Your Type System

#181

Post by someone_19 »

josephg wrote: post #25
pclowes wrote: post #3

I like this. Very much falls into the "make bad state unrepresentable". The issues I see with this approach is when developers stop at this first level of type implementation. Everything is a type and nothing works well together, tons of types seem to be subtle permutations of each other, things get hard to reason about etc. In systems like that I would actually rather be writing a weakly typed dynamic language like…

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…

You can do this quite easily in Rust. But you have to overload operators to make your type make sense. That's also possible, you just need to define what type you get after dividing your type by a regular number and vice versa a regular number by your type. Or what should happen if when adding two of your types the sum is higher than the maximum value. This is quite verbose. Which can be done with generics or macros.

Re: Use Your Type System

#182

Post by somethingsome »

tomtom1337 wrote: post #155
somethingsome wrote: post #143

I'm curious about what you think about something, Supoose you make two simple types one for Kelvin K and the other for Fahrenheit F or degrees D. And you implement the conversions between them in the types. But then you have something like d: D = 10; For i=1...100000: k=f_Take_D_Return_K(d) d=g_Take_K_Return_D(k) end Then you will implicitly have many many automatic conversions that are not useful. How to handle this…

I interpret your question as «given that I am doing many conversions between temperature, because that makes it easier to write correct code, then I worry that my code will be slow because I am doing many conversions». My response is: these conversions are unlikely to be the slow step in your code, don’t worry about it. I do agree though, that it would be nice if the compiler could simplify the math to remove the con…

That's exactly the problem, in the software I have in mind, the conversions are actually very slow, and I can't easily change the content of the functions that process the data, they are very mathematical, it would take much time to rewrite everything.

For example, it's not my case but it's like having to convert between two image representations (matrix multiply each pixel) every time.

I'm scared that this kind of 'automatic conversion' slowness will be extremely difficult to debug and to monitor.

Re: Use Your Type System

#183

Post by alex_smart »

lock1 wrote: post #103
bcrosby95 wrote: post #63

Earlier quoted context omitted.

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…

If only Java also provided Either -like in the standard library... Personally I use checked exceptions whenever I can't use Either and avoid unchecked like a plague. Yeah, it's pretty sad Java language designer just completely deserted exception handling. I don't think there's any kind of improvement related to exceptions between Java 8 and 24.

Ok please help me understand, what is the difference between - R method() throws L, and - Either method()

To me they seem completely isomorphic?

Re: Use Your Type System

#184

Post by idbehold »

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.

>But it takes a while

*Checks watch*

We're going on 45 years now.

Re: Use Your Type System

#185

Post by alex_smart »

default-kramer wrote: post #53
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 checked exceptions were maligned because they were overused. I like that Java supports both checked and unchecked exceptions. But IMO checked exceptions should only be used for what Eric Lippert calls "exogenous" exceptions [1]; and even then most of them should probably be converted to an unchecked exception once they leave the library code that throws them. For example, it's always possible that your DB cou…

>you probably don't want "throws SQLException" polluting the type signature all the way up the call stack

A problem easily solved by writing business logic in pure java code without any IO and handling the exceptions gracefully at the boundary.

Re: Use Your Type System

#186

Post by spookie »

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.

Well, ada is practical

Re: Use Your Type System

#187

Post by someone_19 »

Jtsummers wrote: post #50
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…

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…

Unhappy way is a part of contract. So yes, that is what I want. If a function couldn't fail before but can after the update - I want to know about it.

In fact, at each layer, if you want to propagate an error, you have to convert it to one specific to that layer.

Re: Use Your Type System

#188

Post by vborovikov »

rjbwork wrote: post #80
SideburnsOfDoom wrote: post #60

Earlier quoted context omitted.

There are libraries for that, such as Vogen https://github.com/SteveDunn/Vogen The name means "Value Object Generator" as it uses Source generation to generate the "Value object" types. That readme has links to similar libraries and further reading.

Have you used this in production? It seems appealing but seems so anti-thetical to the common sorts of engineering cultures I've seen where this sort of rigorous thinking does not exactly abound.

Source generators hide too many details from the user.

I prefer to have the generated code to be the part of the code repo. That's why I use code templates instead of source generators. But a properly constructed ID type has a non-trivial amount of code: https://github.com/vborovikov/pwsh/blob/main/Templates/ItemT...

Re: Use Your Type System

#189

Post by ninetyninenine »

giraffe_lady wrote: post #123
ninetyninenine wrote: post #78

Earlier quoted context omitted.

This can be done in typescript. It’s not super well known because of typescripts association with frontend and JavaScript. But typescript is a language with one of the most powerful type systems ever. Among the popular languages like golang, rust or python typescript has the most powerful type system. How about a type with a number constrained between 0 and 10? You can already do this in typescript. type onetonine =…

Typescript's type system is turing complete, so you can do basically anything with it if this sort of thing is fun to you. Which is pretty much my problem with it: this sort of thing can be fun, feels intellectually stimulating. But the added power doesn't make coding easier or make the code more sound. I've heard this sort of thing called the "type puzzle trap" and I agree with that. I'll take a modern hindley milne…

>Which is pretty much my problem with it: this sort of thing can be fun, feels intellectually stimulating. But the added power doesn't make coding easier or make the code more sound.

In practice nobody goes too crazy with it. You have a problem with a feature almost nobody uses. It's there and Range is like the upper bound of complexity I've seen in production but that is literally extremely rare as well.

There is no "temptation" of coding complex logic in it at all as the language doesn't promote these features at all. It's just available if needed. It's not well known but typescript types can be easily used to be 1 to 1 with any hindley milner variant. It's the reputational baggage of JS and frontend that keeps this fact from being well known.

In short: Typescript is more powerful then hindley milner, a subset of it has one to one parity with it, the parts that are more powerful then hindley milner aren't popular and used that widely nor does the flow of the language itself promote there usage. The feature is just there if you need it.

If you want a language where you do this stuff in practice take a look at Idris. That language has these features built into the language AND it's an ML style language like haskell.

Re: Use Your Type System

#190

Post by worldsayshi »

alex_smart wrote: post #183
lock1 wrote: post #103

Earlier quoted context omitted.

If only Java also provided Either -like in the standard library... Personally I use checked exceptions whenever I can't use Either and avoid unchecked like a plague. Yeah, it's pretty sad Java language designer just completely deserted exception handling. I don't think there's any kind of improvement related to exceptions between Java 8 and 24.

Ok please help me understand, what is the difference between - R method() throws L, and - Either method() To me they seem completely isomorphic?

Don't you mean "isosemantic"? Since the same concept is represented with different syntax.
Post reply on HN