Ad hoc type restriction

[Aaryn Tonita]

> I think the best bet for making this usable would be some mechanism like a "view", likely only on value types, that would erase down to the underlying wrapped type, but interpose yourself on construction, and provided a conversion from T to RefinedT that verified the requirement. But this is both nontrivial and presumes a lot of stuff we don't even have yet....

Bringing the newtype pattern to java would be quite handy. Besides these cases of standing in for refinement types there are also all the cases of favoring composition over inheritance where a mechanism to automatically "dereference" to a delegate would avoid a bunch of boilerplate.

-------- Original Message --------
On 10/11/25 00:28, Brian Goetz  wrote:

> There is a literature on "restriction types" or "refinement types" that describes what you are appealing to. It is most commonly used in functional languages to describe restrictions on construction that otherwise would not affect the representation, such as "positive integer" as a restriction of Integer or "sorted list" as a restriction of List. (This is a good match for functional languages because (a) if you avoid putting a bad value into a variable in the first place, you don't have to worry about that changing, and (b) there is no extension, so once you restrict the value of a variable the functions that operate on the underlying type just work on the refined type.)
>
> Liquid Haskell (https://en.wikipedia.org/wiki/Liquid_Haskell, https://ucsd-progsys.github.io/liquidhaskell/) is an experimental variant of Haskell that supports refinement types, in aid of verifiable correctness.
>
> Clojure Spec also can be thought of as a refinement type system, allowing you to use linguistic predicates to overlay optional constraints over an otherwise mostly-dynamically-typed system, such as "the value associated with the map key `age` is a non-negative integer."
>
> The bad news is that proving type safety when restrictions can contain arbitrary predicative logic is ... hard. Liquid Haskell, and other similar systems, often must appeal to SMT/SAT solvers to type-check a program (which is to say that we should not be surprised to find NP-complete problems arising as part of type checking.)
>
> Object-oriented languages like Java would likely get to refinement types through wrapping, which has its own set of limitations. If the type you are refining is an interface, you're fine, but if it is a final class (like all value classes!) you obviously have a problem, because you can't interoperate easily between Integer and RefinedInteger (though this problem is likely solveable for values.)
>
>> But doing that is not ideal because:
>>
>> - This doesn't work for primitive types (e.g., a person's age, grade point average, number of children, etc.)
>> - A wrapper class loses all of the functionality that comes with the wrapped class. For example, I can't say pn1.startsWith(pn2) even though both values are essentially just Strings.
>> - There is performance overhead
>
> (2) is even worse than it sounds: I can't use a WrappedString where a String is expected, even if I manually lifted all the String methods onto it.
>
>> Thoughts?
>
> I think the best bet for making this usable would be some mechanism like a "view", likely only on value types, that would erase down to the underlying wrapped type, but interpose yourself on construction, and provided a conversion from T to RefinedT that verified the requirement. But this is both nontrivial and presumes a lot of stuff we don't even have yet....
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20251011/e307113d/attachment.htm>