Document stability and realizability

Author: Blaisorblade

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

@@ -50,7 +50,15 @@ object CheckRealizable {
   private val LateInitialized = Lazy | Erased
 }
 
-/** Compute realizability status */
+/** Compute realizability status.
+  *
+  * A type T is realizable iff it is inhabited by non-null values. This ensures that its type members have good bounds
+  * (in the sense from DOT papers). A type projection T#L is legal if T is realizable, and can be understood as
+  * Scala 2's `v.L forSome { val v: T }`.
+  *
+  * In general, a realizable type can have multiple inhabitants, hence it need not be stable (in the sense of
+  * Type.isStable).
+  */
 class CheckRealizable(implicit ctx: Context) {
   import CheckRealizable._
 
@@ -66,6 +74,15 @@ class CheckRealizable(implicit ctx: Context) {
 
   /** The realizability status of given type `tp`*/
   def realizability(tp: Type): Realizability = tp.dealias match {
+    /*
+     * A `TermRef` for a path `p` is realizable if
+     * - `p`'s type is stable and realizable, or
+     * - its underlying path is idempotent (that is, *stable*), total, and not null.
+     * We don't check yet the "not null" clause: that will require null-safety checking.
+     *
+     * We assume that stability of tp.prefix is checked elsewhere, since that's necessary for the path to be legal in
+     * the first place.
+     */
     case tp: TermRef =>
       val sym = tp.symbol
       lazy val tpInfoRealizable = realizability(tp.info)
@@ -86,7 +103,11 @@ class CheckRealizable(implicit ctx: Context) {
           if (sym.isStableMember) sym.setFlag(StableRealizable) // it's known to be stable and realizable
           realizability(tp.prefix)
         } mapError { r =>
-          if (tp.info.isStable && tpInfoRealizable == Realizable) Realizable else r
+          // A mutable path is in fact stable and realizable if it has a realizable singleton type.
+          if (tp.info.isStable && tpInfoRealizable == Realizable) {
+            sym.setFlag(StableRealizable)
+            Realizable
+          } else r
         }
       }
     case _: SingletonType | NoPrefix =>

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

@@ -608,7 +608,16 @@ object SymDenotations {
          }
       )
 
-    /** Is this a denotation of a stable term (or an arbitrary type)? */
+    /** Is this a denotation of a stable term (or an arbitrary type)?
+      * Terms are stable if they are idempotent (as in TreeInfo.Idempotent): that is, they always return the same value,
+      * if any.
+      *
+      * A *member* is stable, basically, if it behaves like a field projection: that is, it projects a constant result
+      * out of its owner.
+      *
+      * However, a stable member might not yet be initialized (if it is an object or anyhow lazy).
+      * So the first call to a stable member might fail and/or produce side effects.
+      */
     final def isStableMember(implicit ctx: Context): Boolean = {
       def isUnstableValue = is(UnstableValue) || info.isInstanceOf[ExprType]
       isType || is(StableRealizable) || !isUnstableValue

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

@@ -147,7 +147,11 @@ object Types {
     /** Is this a value type or a wildcard? */
     final def isValueTypeOrWildcard: Boolean = isValueType || this.isInstanceOf[WildcardType]
 
-    /** Does this type denote a stable reference (i.e. singleton type)? */
+    /** Does this type denote a stable reference (i.e. singleton type)?
+      *
+      * Like in isStableMember, "stability" means idempotence.
+      * Rationale: If an expression has a stable type, the expression must be idempotent, so stable types
+      * must be singleton types of stable expressions. */
     final def isStable(implicit ctx: Context): Boolean = stripTypeVar match {
       case tp: TermRef => tp.symbol.isStableMember && tp.prefix.isStable || tp.info.isStable
       case _: SingletonType | NoPrefix => true
@@ -2200,6 +2204,8 @@ object Types {
     def underlyingRef: TermRef
   }
 
+  /** The singleton type for path prefix#myDesignator.
+    */
   abstract case class TermRef(override val prefix: Type,
                               private var myDesignator: Designator)
     extends NamedType with SingletonType with ImplicitRef {