Dotty with explicit nulls #6344
Conversation
|
Can the design doc at https://github.com/abeln/explicit-null-docs/blob/master/design.md serve that purpose? |
That would be a great start. What we should still do is:
|
|
@odersky added the documentation. PTAL. |
abeln
force-pushed
the
dotty-explicit-nulls
branch
from
33d975d to
1694a4a
Compare
|
Rebased. Thanks for the comments. Keep 'em coming! |
|
test performance please |
|
performance test scheduled: 2 job(s) in queue, 1 running. |
|
Performance test finished successfully: Visit http://dotty-bench.epfl.ch/6344/ to see the changes. Benchmarks is based on merging with master (1521576) |
compiler/src/dotty/tools/dotc/core/classfile/ClassfileParser.scala
Outdated
Show resolved
Hide resolved
| case tree: ValDef if ctx.explicitNulls && ctx.owner.is(Method) && !tree.mods.is(Lazy | Implicit) => | ||
| // Use a completer that completes itself with the completion text, so | ||
| // we can use flow typing for `ValDef`s. | ||
| new ValDefInBlockCompleter(tree)(cctx) |
There was a problem hiding this comment.
why not for implicit and lazy ?
There was a problem hiding this comment.
Added a comment:
// Don't use this special kind of completer for lazy or implicit symbols,
// because those could be completed through a forward reference:
// e.g.
// val x: String|Null = ???
// y /* y is completed through a forward reference! */
// if (x == null) throw new NullPointerException()
// lazy val y: Int = x.length
There was a problem hiding this comment.
How do you know these are the only cases that could go wrong? I believe right fix is not to have a ValDefInBlockCompleter and to drop this part.
|
@liufengyun thanks for the comments. Will take a look today. |
There was a problem hiding this comment.
From the GADT perspective: the "special" TermRef approach in this PR works far better than what we currently get with GADT constraints, so we don't want to change anything in that regard.
In the future, instead of using GADT constraints for non-null types, we may actually want to create special TermRefs for terms affected by GADT constraints - among other things, this would likely fix the member lookup problem in #6323.
abeln
force-pushed
the
dotty-explicit-nulls
branch
from
1694a4a to
dc60abc
Compare
|
@odersky would you like to take a look at this (particularly the flow typing part)? |
|
I'll get to this now. |
There was a problem hiding this comment.
So far I reviewed only the architectural design, not so much the code in detail. What I saw was very nice, well explained and of high quality. I do have some feed back on the architecture, though:
The most important issues are:
- There should be no RefEq trait
- The approach to NonNullTermRefs and ValDefInBlockCompleter each violate hard design principles of the compiler and need to be rethought.
Details are in individual comments. I'll wait until these points are addressed and then give it another round.
| final class NonNullTermRef(prefix: Type, designator: Designator) extends TermRef(prefix, designator) { | ||
| // There's nothing special about this class: it's just used as a marker to identify certain | ||
| // `TermRef`s in `computeDenot`. | ||
| } |
There was a problem hiding this comment.
In fact, I don't think this will work. Since TermRef is declared as cached, it has to satisfy that protocol. But NonNullTermRef is not cached. This will cause problems. Probably only in rare situations, but when they arise they will be impossibly hard to debug.
| final class NonNullTermRef(prefix: Type, designator: Designator) extends TermRef(prefix, designator) { | ||
| // There's nothing special about this class: it's just used as a marker to identify certain | ||
| // `TermRef`s in `computeDenot`. | ||
| } |
There was a problem hiding this comment.
It might be better to work on the denotation instead. Use a normal TermRef, but give it a special denotation that strips nulls.
|
@odersky I'm working through the requested changes, but I have a question about
I tried using a normal class Test {
def foo(): Unit = {
val x: String|Null = ???
if (x != null) {
val y = x.length
} else {
val y = x
}
}The problem is that since More generally, there seems to be the assumption in
I think 1) would probably be the less-invasive option, and it's nice to keep the invariant that all TermRefs are cached, but I don't have a good sense for the performance implications. Any thoughts? |
|
@abeln I think your reasons for not using Some info in caching:
|
|
A (non) update on this. I'm still looking into how to cache NonNullTermRefs (as well as at Martin's other comments). I'm away on vacation for next week, and will get back to this when I'm back. |
|
@abeln OK, we can wait a bit. The plan is to announce at Scala Days that we have fixed our "feature envelope" for 3.0. This is not yet a feature freeze, so some changes are still possible. But new features other than the ones we have now will have to wait for later versions. We can include explicit nulls provisionally in that envelope. They'd need to be fully worked out and tested by the time we go into real feature freeze later this year. |
abeln
force-pushed
the
dotty-explicit-nulls
branch
3 times, most recently
from
241f8d7 to
8fc0113
Compare
|
#7520 is bascically done now. It implements flow analysis for nullability that works for vals as well as vars. The results of the analysis are contained in the There are also some new developments which should simplify the treatment afterwards. There's a new trait (right now we need a cast at the end, but this will go away one we have integrated flow analysis with the rest of explicit nulls). Using the method, we use normal typing to determine that if This means we don't need So, I propose we rework the present PR to go with #7520. In particular
WDYT? |
|
@odersky this sounds great. We had trouble with Does class Foo {
type T = String
}
val x: Foo|Null = ???
if (x != null) {
// x: String
val y: x.T = "hello" // this should work, right?
}However, if we wrap non null TermRefs in calls to val x: Foo|Null = ???
if (x != null) {
val y: notNull(x).T = "hello" // error: notNull(x) is not stable
}Also, what about interactions between flow typing and implicits? def foo(implicit s: String) = ???
implicit val x: String|Null = ???
if (x != null) {
foo
}It seems like the call to I'll send you my comments for #7520 today, but the code is very nice and I'm glad you got the |
|
I like the code in #7520 and I agree that we should rebase the explicit nulls PR to use it. I read the code and did not have any low level comments, but I think @abeln has some. I really like the idea of the Is the eventual plan to remove or inline the |
|
@abeln inside a path-dependent type, we don't need the non-nullness information, do we? So can't we just not wrap the Regarding implicits, are they not rewritten to explicit parameter passing in the typer? So that code would need to look in the context for the nullness information and rewrite the call |
If we don't wrap the
Ok, so the implicit resolution logic will have to take the new non-null information into account. |
|
I wonder if we can make this PR an opt-out feature. A developer must |
|
@Atry right now the changes are opt-in (you have to set '-Yexplicit-nulls' for the type system changes to kick in). Once we're more confident that things are working well (better testing, the compiler bootstraps with explicit nulls, etc), I imagine we'd turn it on by default (in which case we'd probably want opt-outs like you mention). |
|
In spite of the opt-in vs opt-out debate, what matters is the ability to
enable or disable the feature per file.
Abel Nieto <notifications@github.com>于2019年11月12日 周二下午6:38写道：
… @Atry <https://github.com/Atry> right now the changes are opt-in (you
have to set '-Yexplicit-nulls' for the type system changes to kick in).
Once we're more confident that things are working well (better testing, the
compiler bootstraps with explicit nulls, etc), I imagine we'd turn it on by
default (in which case we'd probably want opt-outs like you mention).
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#6344>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAES3OQRO5YDMRT5ZAIEDELQTNSCJANCNFSM4HHA3F3A>
.
|
|
You can't make this per file, because it changes subtyping, and subtyping is a global function, with caches, inter-file dependencies, etc. So unfortunately that's not going to happen, however desirable it can be. |
|
An alternative definition of def notNull[A](x: A | Null): x.type & A = {
assert(x != null)
x.asInstanceOf[x.type & A]
}Besides not requiring Really the introduction of |
We can use the technology similar to Java Interop. When type-checking an explicitly-declared type tree or a // LegacyClass.scala
import scala.language.uncheckedNull
case class LegacyClass()
object LegacyClass {
// Inferred as LegacyClass | Null
def newLegacyClass = new LegacyClass()
// Inferred as LegacyClass | Null
def legacyClass = LegacyClass()
// Inferred as NullSafeClass | Null
def newNullSafeClass = new NullSafeClass()
// Inferred as NullSafeClass
def nullSafeClass = NullSafeClass()
// Patched as NullSafeClass | Null
def explicitlyTypedNullSafeClass: NullSafeClass = NullSafeClass()
// compiles because the type is patched as ((LegacyClass | Null) <:< Null) | Null
implicitly[LegacyClass <:< Null]
// compiles because the type is patched as ((NullSafeClass | Null) <:< Null) | Null
implicitly[NullSafeClass <:< Null]
}// NullSafeClass.scala
case class NullSafeClass()
object NullSafeClass {
// Inferred as LegacyClass
def newLegacyClass = new LegacyClass()
// Inferred as LegacyClass | JavaNull
def legacyClass = LegacyClass()
// Does not compile
// def legacyClass: LegacyClass = LegacyClass()
// Inferred as NullSafeClass
def newNullSafeClass = new NullSafeClass()
// Inferred as NullSafeClass
def nullSafeClass = NullSafeClass()
// Does not compile
// implicitly[LegacyClass <:< Null]
// Does not compile
// implicitly[NullSafeClass <:< Null]
} |
|
Or we can create a deprecated implicit conversion for migration. @deprecated(since="3.0", message="Unchecked null")
implicit def notNull[A](x: A | Null): x.type & A = {
x.asInstanceOf[x.type & A]
} |
Here's a refinement that also addresses the issue @abeln had with path types (I agree this is a real problem): Make This means that At first, I was tempted to merge @srjd: In this design One could discuss whether we should make |
|
@sjrd A systematic way to generalize what we do for |
|
You don't need a full generalization to def notNull(tpe: Type): Type =
tpe & TypeRef(NotNullClass)The only reason this is useful is because Instead of inventing def notNull(tpe: Type): Type = tpe match {
case _ if tpe.isRef(NullClass) => NothingClass
case UnionType(tp1, tp2) => notNull(tp1) | notNull(tp2)
case _ => tpe
}This is not technically as precise as And that strategy you can actually generalize to arbitrary def typeSubtract(tp1: Type, tp2: Type): Type = tp1 match {
case _ if tp1 <:< tp2 => NothingClass
case UnionType(tp11, tp12) => typeSubtract(tp11, tp2) | typeSubtract(tp12, tp2)
case _ => tp1
}For the purposes of flow typing, this is really all you need to write useful programs. For a branch of the form val x: T = ...
if (x.isInstanceOf[U]) {
// here x: U
} else {
// here x: typeSubtract(T, U)
}When val y: A = xin the This design will be significantly simpler than what you are proposing with |
|
@sjrd we already have a method like It seems that if we only have The example I gave above class Foo {
type T = String
}
val x: Foo|Null = ???
if (x != null) {
// x: String
val y: x.T = "hello" // this should work, right?
}The solution that Martin suggested class Any
final val $nn: this.type & NotNulland then we expand This requires having a |
|
Also notice that @odersky's def notNull(x: Any): x.type & NotNull =
assert(x != null)
xwhile @sjrd's def notNull(tpe: Type): Type = tpe match {
case _ if tpe.isRef(NullClass) => NothingClass
case UnionType(tp1, tp2) => notNull(tp1) | notNull(tp2)
case _ => tpe
}I suggest we use different names; otherwise it's gonna get confusing :)
We are not adding the calls to (the user level) |
|
OK I'm going to use Using my version of the library def notNull[A](x: A | Null): x.type & A = {
assert(x != null)
x.asInstanceOf[x.type & A] // safe
}then you have compiler code that can insert calls to |
|
The example with the path-dependent type that should be valid under flow typing is not supported by my idea, but you can make it work by writing the user program a bit differently: class Foo {
type T = String
}
val x: Foo|Null = ???
if (x != null) {
val x2: x.type & Foo = x
val y: x2.T = "hello" // this now works
}I'd like to see real world examples of path-dependent types used under |
|
It's nice that What would we do with path-dependent types; i.e. #6344 (comment) ? EDIT: I see your comment now :) |
Cross-post. See my comment above yours ;) |
I agree that this seems rare. In fact, in our experiments so far, any use of flow typing seems relatively rate (we'll have results to show soon). Since there is a workaround, I would be ok with implementing the scheme without the |
|
I think just because something is not yet used in our examples does not mean we can ignore it. We have just scratched the surface with examples; there will be many more use cases to come. I believe the rule in the spec should be as follows:
This is at the same time elegant and powerful. I would not like to have to put in the spec that we do this only for expressions and for types or patterns you have to rewrite the program. Having and for typing a Java-like Map get: In short, Another way to put it is that, if we have a flow analysis that asserts a property X (in this case, being NotNull) then it is natural that X should itself be expressible as a type. Yes, maybe you can work around many of the cases, but why not tackle it directly? And how can we convince ourselves that the workarounds are sufficiently general? |
Does that also hold for flow typing for variables? I would expect flow typing for vals to be rare but flow typing for vars to be quite common. |
13 participants
This PR adds a
-Yexplicit-nullsexperimental flag which, if enabled, modifies the type system so that reference types are non-nullable. Nullability needs then to be expressed explicitly via unions (e.g.String|Null).At a high level, the changes to the compiler are:
Null, as describedif (x != null && x.length < 10))Internal doc: https://gist.github.com/abeln/573cd43ec062ca0ba2dbdae625d26d42
User-facing doc: https://gist.github.com/abeln/ca50cd5a3b94316c586db5c986049d2d