Ad hoc type restriction

Red IO redio.development at gmail.com
Sat Oct 11 16:17:31 UTC 2025


This sounds pretty similar in concept to rust smart pointers. More
precisely the deref operator. It allows the wrapper object to be treated
like a reference to the actual value and as "methods" in rust are called on
references to objects it gets the ability to have all methods called on the
wrapper object. And treated like a temporary reference to the actual
contained value.
This works great because of rusts explicit references, values and the
lifetime system. Applying this concept to Java is possible but isn't as
syntheticly clear like in rust. It requires the notion of a temporary
reference to make sense. Something that doesn't exist in java syntacticly.
Without this concept it's just an implicit cast. Effectively an implicit
getter.
Another problem is that different to rust mutability isn't a property an
instance and all it's fields share but a property all fields decide
separately. Therefore a mutable type cannot be forced to act immutable when
viewed through the restricting wrapper types getter. Java expresses no
ownership relationship between an object and its fields.

For this concept to work and preserve the integrity of the wrappers
restrictions it requires either colored methods (mutable, immutable) or
defensive copies on access. Both are not concepts that have a universal
implementation in Java.

As introducing colored functions is out of the question only defensive
copies are possible. This requires the concept of a copy mechanisms the
compiler can use when accessing the actual value through the restricting
wrapper. This could be a cow (copy on write) or a normal field copy.

Introducing a formal way to make a copy of classes instance is something
that is beneficial anyway and overlaps with some Valhalla concepts.

Hope these thoughts help in the understanding of the problems and possible
solutions.

Great regards
RedIODev

On Sat, Oct 11, 2025, 07:29 Aaryn Tonita <atonita at proton.me> wrote:

>
> > 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:
>
>    1. This doesn't work for primitive types (e.g., a person's age, grade
>    point average, number of children, etc.)
>    2. 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.
>    3. 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/dfec0ec4/attachment-0001.htm>


More information about the amber-dev mailing list