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

251–260 of 357 posts

Re: Use Your Type System

#251

Post by archargelod »

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…

Nim[0] supports subrange types:

  type
    Foo = range[1 .. 10]
    Bar = range[0.0 .. 1.0] # float works too
  
  var f:Foo = 42       # Error: cannot convert 42 to Foo = range 1..10(int)
  var p = Positive 22  # Positive and Natural types are pre-defined
[0] - https://nim-lang.org/docs/manual.html#types-subrange-types

Re: Use Your Type System

#252

Post by lock1 »

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?

That's what I thought at first too. At first glance they look equivalent, telling API users what the expected result of a method call is. In that sense, both are equivalent.

But after experimenting a bit with checked exceptions, I realized how neglected exceptions are in Java. - There's no other way to handle checked exceptions other than try-catch block - They play very badly with API that use functional interfaces. Many APIs don't provide checked throws variant - catch block can't use generic / parameterized type, you need to catch Exception or Throwable then operate on it at runtime

After rolling my own Either, it felt like a customizable typesafe macro for exception handling. It addresses all the annoyances I had with checked exception handling, and it plays nicely with exhaustive pattern matching using `sealed`.

Granted, it has the drawback that sometimes I have to explicitly spell out types due to local type inference failing to do so. But so far it has been a pleasant experience of handling error gracefully.

Re: Use Your Type System

#253

Post by esafak »

ryandrake wrote: post #158
kwon-young wrote: post #142

This reminds me of the mp-units [1] library which aims to solve this problem focusing on the physical quantities. The use of strong quantities means that you can have both safety and complex conversion logic handled automatically, while having generic code not tied to single set of units. I have tried to bring that to the prolog world [2] but I don't think my fellow prolog programmers are very receptive to the idea ^…

I remember a long, long time ago, working on a project that handled lots of different types of physical quantities: distance, speed, temperature, pressure, area, volume, and so on. But they were all just passed around as "float" so you'd every so often run into bugs where a distance was passed where a speed was expected, and it would compile fine but have subtle or obvious runtime defects. Or the API required speed i…

https://nim-by-example.github.io/types/distinct/

https://kotlinlang.org/docs/inline-classes.html

https://www.open-std.org/jtc1/sc22/wg14/www/docs/n3320.htm

https://doc.rust-lang.org/rust-by-example/generics/new_types...

Re: Use Your Type System

#255

Post by ijustlovemath »

steveklabnik wrote: post #32
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…

In my understanding Rust may gain this feature via “pattern types.”

Where can I sign?

Re: Use Your Type System

#256

Post by drpixie »

idbehold wrote: post #184
tylerhou wrote: post #176

Earlier quoted context omitted.

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.

Naaa ... most "new" languages are just reinventions of stuff that's been around for ... 45 years, by people who should know better.

Re: Use Your Type System

#257

Post by drpixie »

bbkane wrote: post #19

I was doing this and used it for a year in https://github.com/bbkane/warg/ , but ripped it out since Go auto-casts underlying types to derived types in function calls: Type userID int64 func Work(u userID) {...} Work(1) // Go accepts this I think I recalled that correctly. Since things like that were most of what I was doing I didn't feel the safety benefit in many places, but had to remember to cast the type in othe…

Arrggg- that's the best reason, so far, to avoid Go.

Almost nothing is a number. A length is not a number, an age is not a number, a phone number is not a number - sin(2inches) is meaningless, 30years^2 is meaningless, phone#*2 is meaningless, and 2inches+30years is certainly meaningless - but most of our languages permit us to construct, and use, and confuse these meaningless things.

Re: Use Your Type System

#258

Post by wavemode »

Jensson wrote: post #236
materiallie wrote: post #159

Earlier quoted context omitted.

Put another way: errors tend to either be handled "close by" or "far away", but rarely "in the middle". So Java's checked exceptions force you to write verbose and pointless code in all the wrong places (the "in the middle" code that can't handle and doesn't care about the exception).

> So Java's checked exceptions force you to write verbose and pointless code in all the wrong places (the "in the middle" code that can't handle and doesn't care about the exception). It doesn't, you can just declare that the function throws these as well, you don't have to handle it directly.

It pollutes type signatures. If some method deep down the call stack changes its implementation details from throwing exception A you don't care about to throwing exception B you also don't care about, you also have to change the type of `throws` annotation on your method.

This is annoying enough to deal with in concrete code, but interfaces make it a nightmare.

Re: Use Your Type System

#259

Post by jjmarr »

mcculley wrote: post #55
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…

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

VHDL has this feature too, being based on Ada.

Re: Use Your Type System

#260

Post by [deleted] »

Conscat wrote: post #199
henry700 wrote: post #108

Earlier quoted context omitted.

The natural solution for this is a private constructor with public static factory methods, so that the user can only obtain an instance (or the error result) by calling the factory methods. Constructors need to be constrained to return an instance of the class, otherwise they would just be normal methods. Convention in OOP languages is (un?)fortunately to just throw an exception though.

In languages with generic types such as C++, you generally need free factory functions rather than static member functions so that type deduction can work.

[deleted]
Post reply on HN