-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add experimental flexible types feature on top of explicit nulls #17369
Conversation
Enabled by -Yflexible-types with -Yexplicit-nulls. A flexible type T! is a non-denotable type such that T <: T! <: T|Null and T|Null <: T! <: T. Here we patch return types and parameter types of Java methods and fields to use flexible types. This is unsound and kills subtyping transitivity but makes interop with Java play more nicely with the explicit nulls experimental feature (i.e. fewer nullability casts). Also adds a few tests for flexible types, mostly lifted from the explicit nulls tests.
Intentionally destroying transitivity in an unsound way is worrisome. Granted, the Scala type system already lacks transitivity, in the sense that there exist triples of This experimental features introduces an explicitly unsound subtyping relationship through broken transitivity. This kind of hole can create real problems. I assume you've considered alternatives such as using implicit conversions for the "down casts" instead of actual subtyping. If yes, what were the problems that that caused? In other words, what trade-off in your opinion justifies to break subtyping ? |
It's similar to what Kotlin does with their platform types. In Scala there is a "natural" way to express such a type as an abstract type with some specific bad bounds. |
I'm not sure if this design choice has been considered or not: Don't use types for enforcing null-safety while interop with Java, use local analysis. To be clear, I mean keeping the subtyping change for
Benefits:
|
The unsafe nulls language import allows to locally suspend null safety. When interacting with Java, suspending null safety is not enough. Sometimes the compiler needs to choose some specific type and no specific choice is always best (whether we meet "best" in the sense of soundness or "best" in the sense of lack of compile-time errors). For example: val x = "foo".split(" ") We need to pick some type for |
If such code does not pose a problem without explicit-null, then it seems taking the Java signature as it is will avoid usability issues. |
@@ -77,12 +77,12 @@ object JavaNullInterop { | |||
* If tp is a type of a field, the inside of the type is nullified, | |||
* but the result type is not nullable. | |||
*/ | |||
private def nullifyExceptReturnType(tp: Type)(using Context): Type = | |||
new JavaNullMap(true)(tp) | |||
private def nullifyExceptReturnType(tp: Type, ownerIsClass: Boolean)(using Context): Type = |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think we need to modify nullifyExceptReturnType
? It is a separate feature.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Did you mean it's for unsafe-java-return? It looks like that's not what it's used for. See the call to nullifyExceptReturnType
above.
Closing, continued in #18112. |
…cit-nulls (#18112) This is a continuation of #17369. When dealing with reference types from Java, it's essential to address the implicit nullability of these types. The most accurate way to represent them in Scala is to use nullable types, though working with lots of nullable types directly can be annoying. To streamline interactions with Java libraries, we introduce the concept of flexible types. The flexible type, denoted by `T?`, functions as an abstract type with unique bounds: `T | Null ... T`, ensuring that `T | Null <: T? <: T`. The subtyping rule treats a reference type coming from Java as either nullable or non-nullable depending on the context. This concept draws inspiration from Kotlin's [platform types](https://kotlinlang.org/docs/java-interop.html#null-safety-and-platform-types). By relaxing null checks for such types, Scala aligns its safety guarantees with those of Java. Notably, flexible types are non-denotable, meaning users cannot explicitly write them in the code; only the compiler can construct or infer these types. Consequently, a value with a flexible type can serve as both a nullable and non-nullable value. Additionally, both nullable and non-nullable values can be passed as parameters with flexible types during function calls. Invoking the member functions of a flexible type is allowed, but it can trigger a `NullPointerException` if the value is indeed `null` during runtime. ```scala // Considering class J is from Java class J { // Translates to def f(s: String?): Unit public void f(String s) { } // Translates to def g(): String? public String g() { return ""; } } // Use J in Scala def useJ(j: J) = val x1: String = "" val x2: String | Null = null j.f(x1) // Passing String to String? j.f(x2) // Passing String | Null to String? j.f(null) // Passing Null to String? // Assign String? to String val y1: String = j.g() // Assign String? to String | Null val y2: String | Null = j.g() // Calling member functions on flexible types j.g().trim().length() ```
This PR adds an experimental flag
-Yflexible-types
which pairs with-Yexplicit-nulls
to enable flexible types. This builds on the explicit nulls experimental feature to make interoperation with Java code less cast-ful.A flexible type of
T
(here, writtenT!
for convenience) is defined such thatT <: T!
andT! <: T|Null
, but alsoT|Null <: T!
andT! <: T
.These flexible types are non-denotable and are patched into the return types and parameter types of Java methods. For example, a Java method
String foo(String s)
becomesfoo(s: String!): String!
, so that either an instance ofString
orString|Null
may be passed tofoo
, andfoo(s)
may be assigned to aString
or aString|Null
.This is technically unsound and kills subtyping transitivity, but makes the explicit nulls feature play more nicely with Java code so that adoption of explicit nulls can be encouraged. Attempting to compile the community build results in strictly fewer errors than with explicit nulls only, with some projects (effpi, monocle, munitsCatsEffect, libretto) being coaxed into compiling without any errors.
Note that this, like explicit nulls, suffers from the problem described in #15194.
This could also potentially be implemented as a language import rather than as a flag.