Ad hoc type restriction

[Brian Goetz]

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 saypn1.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/20251010/445bab68/attachment.htm>