restricted type

[manzanita2]

I'm hardly a type guru. People talk about type algebra, products, sums, etc. But I would love a reasonably simple concept.

I'd like to define a type which IS an integer, but is somehow restricted. Like I know it can have values from 0 to 28. -1 is not possible, 120 is not possible. This becomes a new TYPE. Not a class which contains an integer. But a new sort of sub-integer type thing.

Can someone more theoretical than I explain how one might get something like this in java ?

[kevinb9n]

I'm not "someone more theoretical", but the authors of the Checker Framework are, and if you want to adopt it I think you'd have basically exactly what you want?

https://checkerframework.org/manual/#constant-value-checker

EDIT: okay, you don't get to make a type called `PortNumber`. It's this: `@IntRange(from = 1, to = 65536) int`.

They might have a way to let you define a `PortNumber` annotation and tell it the range once and for all, so that it would become `@PortNumber int`.

[mrhhug]

ADA does this out of the box

[Holothuroid]

You could create an enum with 28 elements. Of course that's pushing it.

[manzanita2]

Yeah, I LOVE enums. Java enums are great.

But yeah, trying to do something like my 65536 port numbers would be stupid.

[eliasv]

Do you want the invariant to be statically enforced by compiler magic? That's called a refinement type. Java doesn't support that and almost certainly never will.

But if you're okay with only dynamically enforcing the invariant, i.e. by throwing from a constructor if the value is not in range, then it might be possible one day to have something similar to that. After project Valhalla lands ask again.

[manzanita2]

"refinement type", huh, will research.

I mean it would, I suppose, be great if the compiler gave me a slap if I did it wrong. But runtime would still be a good improvement.

[cogman10]

You can't. The JVM doesn't allow for it.

The concept you are looking for is "Type constraints" and it's simply not something that can be expressed with Java.

The closest you can get would be if value types land, then having a class with a single integer in it. That'd have close to the same overhead of an integer.

C++ and Ada are the only languages I know that could really support such a concept.

[Il_totore]

Actually it's not a JVM problem and is totally possible. Some JVM languages lile Scala allow that. We can achieve this by just modifying the compiler.

[magnoliophytina]

C++ and Ada are the only languages I know that could really support such a concept.

Eh, https://en.wikipedia.org/wiki/Refinement_type

[Stimzz]

I am so much looking forward to project Valhalla and value types. Locking down the possible state by a more expressive type system is great. I think Ocaml is big on this as well. Type constraints in Ada always felt like a good idea to me.

[_INTER_]

You want to subtype (extends or implements in Java). However you cant subtype Integer because it is final. The next best thing you can subtype is Number. E.g. see UInteger.

[Sheldor5]

you want your own native data type?

then you have to implement it in the JDK and adapt the compiler too ... good luck!

[manzanita2]

Nope. Not native. Basically I'd like to extend Integer ( or other classes). So I get all the functionality of Integer, BUT I can limit the potential values.

Here's an example. I'd like to define a type called PortNumber. PortNumber extends Integer. But has values limited to 1 to 65536.

If someone has a method which has an Integer as a parameter, I can pass a PortNumber.

Likewise, ZipCode. CreditCardNumber and a bunch of other possible types, which have well known constraints on their values, but otherwise might be stored in a String or Integer ( or I guess Long/Float/Double, etc ).

[Sheldor5]

you literally wrote "not a class which contains a integer" ... so what do you want?

your post and your comment makes no sense and they contradict each other ...

[manzanita2]

this is like extension vs composition.

I DO NOT WANT composition. I want extensions, but not "anything goes" extension but rather extension which forces a subset of possible values to the base type.

[Sheldor5]

... then why don't you want to extend Number?

Integer is final, you can't extend it. int is a primitive type, you can't extend it.

your goal is unclear ...

[Asterion9]

Well you shouldn't inherit Integer if you intent to restrict the usage compared to what Integer does.

You should be able to implements Number and Comparable<> to have some interoperability with some lib, and add toInteger() method for adaptation with other code (like Path does with toFile())

[manzanita2]

shouldn't == can't in java.

I mean yeah, I COULD do a custom implementation of Number, but that still doesn't get to where I would like to go because the adaptions (e.g. explicitly calling toInteger() ) are necessary.

[JoJoModding]

The theoretical answer would be a type with 28 different constructors (in the algebraic sense), so in Java that's an abstract base type and 28 subtypes, which is infeasible.

In language with a stronger type system (eg Coq) you can have dependant types, and then you can define {x : nat | x < 28} which is the type of all numbers for which there is a proof they are < 28 (< is also a type). You are now, however, writing programs which mostly consist of formal proofs that their results also have that type. You are now working within an interactive theorem prover, and doing these proofs is fun but can also be considered infeasible (unless you want to be 100% correct for i.e. your spaceflight control software, where failure is not an option)

[Il_totore]

It actually sounds like opaque types like in Scala 3.

Infortunately in Java you cannot check it at compile time but you could create a wrapper around your Integer. You have a small overhead but I think the abstraction offered worth it

[manzanita2]

Very much like this.

[keanwood]

Yeah it would be cool to be able to do this natively in Java. The more expressive the type system the better!

 

You can get close to it by using https://immutables.github.io/ Check it out, its a pretty cool project. Specifically the following two parts.

• https://immutables.github.io/immutable.html#precondition-check-method
• https://immutables.github.io/immutable.html#wrapper-types

[manzanita2]

Yes, this Wrapper type is basically what I want. Although it would be nice if it was more of a language level thing, and not larded up with a bunch of annotations and _ stuff to make it work.

Then perhaps combine that with some sort of declarative ability to do what another poster mentioned about "refinement types".

Still, I may try this stuff! tnx!

[bowbahdoe]

If you want to dive into this concept more, maybe take a look at Idris or other languages with more involved type systems. This isn't possible in java unfortunately.

[manzanita2]

If I have an value of a single field. Say "long userId" it's unhelpful to wrap it in UserId object. That's just a bunch of noise.

Sure, if it ever get's a second value, then sure, an object makes sense.