Add refining annotations #4626

odersky · 2018-06-07T09:45:07Z

Adds a new kind of annotation that conceptually refines the annotated type. That is, refining annotations yield subtypes. They are more "sticky" than normal annotations. In a number of situations they are not stripped away where normal annotations are.

It is intended that this kind of annotation is a good basis to define TypeOf types.

The idea is that such annotations create some proper subtype of the type they annotate. Hence, they cannot be stripped away like normal annotations are.

- some keep their annotations - some only keep refining annotations - most of them still strip all annotations

odersky · 2018-06-07T10:16:40Z

@gsps I recommend to use this status as a basis for further work.

Next step could be to define an annotation like TypeOf in

library/src/scala/annotation/internal

OlivierBlanvillain

Should ConstantType and TermRef be refactored into AnnotatedType with RefiningAnnotation?

OlivierBlanvillain · 2018-06-07T10:39:35Z

library/src/scala/annotation/RefiningAnnotation.scala

+ *  Refining annotations are more "sticky" than normal ones. They are conceptually kept
+ *  around when normal refinements would also not be stripped away.
+ */
+trait RefiningAnnotation extends StaticAnnotation


Why expose that in the stdlib, isn't this compiler internal only?

No, you might want to define your own annotations (say units of measure). Maybe they need a compiler plugin to order to be checked, or maybe you can do it in the future with annotation macros. RefiningAnnotation just makes sure they propagate correctly.

odersky · 2018-06-07T14:31:05Z

Should ConstantType and TermRef be refactored into AnnotatedType with RefiningAnnotation?

In principle, we could consider this. But these two are a little bit different since they are also the main carriers of singleton types. Also the terms they capture are not very general, so it's not clear what we would win.

gsps

This looks nice! At this point, I'd actually be quite tempted to also add DistributiveRefiningAnnotation along with the appropriate cases to distributiveOr and distributiveAnd ;-)

In any case, I'll give it a shot and try to rebase our WIP transparent PR on this.

gsps · 2018-06-07T18:12:35Z

compiler/src/dotty/tools/dotc/core/Definitions.scala

@@ -694,6 +694,8 @@ class Definitions {
  def ClassfileAnnotationClass(implicit ctx: Context) = ClassfileAnnotationType.symbol.asClass
  lazy val StaticAnnotationType        = ctx.requiredClassRef("scala.annotation.StaticAnnotation")
  def StaticAnnotationClass(implicit ctx: Context) = StaticAnnotationType.symbol.asClass
+  lazy val RefiningAnnotationType        = ctx.requiredClassRef("scala.annotation.RefiningAnnotation")


(Misaligned =)

gsps · 2018-06-07T18:26:49Z

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -283,6 +283,15 @@ object Types {
      case _ => false
    }

+    /** Does this type have a supertype with an annotation satisfying given predicate `p`? */
+    def derivesAnnotWith(p: Annotation => Boolean)(implicit ctx: Context): Boolean = this match {
+      case tp: AnnotatedType => p(tp.annot) || tp.tpe.derivesAnnotWith(p)


Consider renaming AnnotatedType#tpe to #parent or #info? (I find tp.tpe slightly confusing.)

gsps · 2018-06-07T18:28:09Z

compiler/src/dotty/tools/dotc/util/common.scala

@@ -8,6 +8,7 @@ import core.Types.WildcardType
 object common {

  val alwaysTrue = Function.const(true) _
+  val alwaysFalse = Function.const(false) _


Is this used anywhere?

No. I used it in an intermediate version. I kept it for duality.

gsps · 2018-06-07T18:38:11Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -700,7 +705,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
              }
            case tycon1: TypeVar =>
              isMatchingApply(tycon1.underlying)
-            case tycon1: AnnotatedType =>
+            case tycon1: AnnotatedType if !tycon1.isRefining =>


I'm not sure when a type constructor would have a RefiningAnnotation, but wouldn't it in principle be okay to widen here, regardless of whether the annotation is refining?

Yes, well spotted. Narrowing the lower bound is always safe, and it is the only thing we can do in this case.

Looks like this PR was merged without addressing this comment?

gsps · 2018-06-08T13:02:33Z

LGTM.

smarter · 2018-06-08T15:03:20Z

compiler/src/dotty/tools/dotc/core/TypeComparer.scala

@@ -1546,7 +1552,7 @@ class TypeComparer(initctx: Context) extends DotClass with ConstraintHandling {
      }
    case tp1: TypeVar if tp1.isInstantiated =>
      tp1.underlying & tp2
-    case tp1: AnnotatedType =>
+    case tp1: AnnotatedType if !tp1.isRefining =>
      tp1.underlying & tp2


Why not rewrap the annotation around the intersection if it's a refining annotation?

smarter · 2018-06-08T15:05:47Z

compiler/src/dotty/tools/dotc/core/Types.scala


-    override def stripAnnots(implicit ctx: Context): Type = tpe.stripAnnots
+    def isRefining(implicit ctx: Context) = {
+      if (!isRefiningKnown) {


Shouldn't the cache be invalidated at the start of a new run?

I was thinking about that too, but decided that it's probably fine given the internal nature of such annotations. Then again, we do expose RefiningAnnotation in the public scala.annotation package.

smarter · 2018-06-08T15:09:40Z

This PR would really really benefits from having tests.

odersky added 2 commits June 7, 2018 11:13

Introduce RefiningAnnotations

4800cef

The idea is that such annotations create some proper subtype of the type they annotate. Hence, they cannot be stripped away like normal annotations are.

Refine dealiasing operations

10b59f8

- some keep their annotations - some only keep refining annotations - most of them still strip all annotations

odersky mentioned this pull request Jun 7, 2018

Add subtype annotations #4625

Closed

Doc comment RefiningAnnotation class

984afee

odersky requested review from gsps and OlivierBlanvillain June 7, 2018 10:13

OlivierBlanvillain reviewed Jun 7, 2018

View reviewed changes

gsps reviewed Jun 7, 2018

View reviewed changes

Address review comments

81a5cf9

odersky force-pushed the add-refining-annotations branch from a4745fd to 81a5cf9 Compare June 8, 2018 08:00

Fix indentation

dde7ce9

odersky merged commit 25ee50b into scala:master Jun 8, 2018

smarter reviewed Jun 8, 2018

View reviewed changes

allanrenucci deleted the add-refining-annotations branch June 8, 2018 18:35

Add refining annotations #4626

Add refining annotations #4626

Uh oh!

Conversation

odersky commented Jun 7, 2018

Uh oh!

odersky commented Jun 7, 2018

Uh oh!

OlivierBlanvillain left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

odersky commented Jun 7, 2018

Uh oh!

gsps left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

odersky Jun 8, 2018 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

gsps commented Jun 8, 2018

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smarter commented Jun 8, 2018

Uh oh!

Uh oh!

odersky Jun 8, 2018 •

edited

Loading