Opaque types - selftype encoding

[odersky]

A fiendlishly clever way to encode opaque types using a combination of abstract types, self types, and union and intersection types. Refines a suggestion by @adriaanm - that guy has a really twisted mind 😎.

An opaque type / companion object combo

object o {
  opaque type T = U
  object T
}

is represented as

object o {
  type T = T.T
  object T { 
    this: { type T >: U | o.T <: U & o.T } =>
    type T
  }
}

The checking of the self type is omitted (objects can't officially have a self type anyway). The bounds in the self type achieve that inside object T, type T.this.T is known to be an alias of both o.T and U. On the other hand, outside T, o.T is known to be an alias of T.T, but is not known to be an alias of U, since the self type is unavailable outside the object.

[odersky]

Replaces #4028

[odersky]

The actual implementation starts with "Parsing and pickling of opaque types" d8a6f1c. Before is just general polishing and housekeeping.

It is best reviewed commit by commit.

[odersky]

test performance please

[dottybot]

performance test scheduled: 1 job(s) in queue, 0 running.

[dottybot]

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/5300/ to see the changes.

Benchmarks is based on merging with master (2f64743)

[odersky]

Performance tests look good. No apparent degradation.

[odersky]

The bounds in the self type achieve that inside object T, type T.this.T is known to be an alias of both o.T and U.

Some explanations, since it's a subtle point. Inside T, it is known that T.this.tpe = o.T.type, so why is T.this.T not recognized to be equal to o.T or o.T.T? The reason is that the subtype checker will always maximally dealias before comparing. T.this.T dealiases to U while o.T dealiases to o.T.T. The two dealiased types are different.

Normally, this dealiasing strategy should not lose equalities but here we have an irregular situation since the module T claims in its self type more than it can deliver. If we would use one of the encodings of opaque types that does not rely on magic, the dealising would be admissible, but o.T.type would not be recognized as being equal to T.this.type.

The selftype bound

type T >: U | o.T <: U & o.T

compensates for the loss of equalities through dealiasing by explicitly making T.this.T both a subtype and a supertype of o.T.

A similar trick can be played if we rely on abstract type sealing. Here's an alternative version of an opaque encoding:

object o {

  trait T {
    type A
  }

  class C extends T { this: m.type =>
    type A = Int

    def reveal(x: A): Int = x
    def inject(x: Int): A = x

    var a: A = ???
    x = a // error: found: this.A required: m.A
    a = x // error: found: m.A required: this.A
  }

  val m: T = new C
  type A = m.A

  var x: A = ???
}

There are two errors, which show that, again, o.T and T.this.T are not recognized to be equal inside T. But by strengthening the bound for o.T we can recover the information:

object Test {

  trait T {
    type A
  }

  class C extends T { this: m.type =>
    type A >: Int | Test.A <: Int & Test.A

    def reveal(x: A): Int = x
    def inject(x: Int): A = x

    var a: A = ???
    x = a // OK!
    a = x // OK!
  }

  val m: T = new C
  type A = m.A

  var x: A = ???
}

Except that now C is not instantiatable because it contains a type with possibly conflicting bounds. That would need to be fixed separately by introducing a special rule.

[DavidGregory084]

@odersky I'm probably making a foolish-sounding observation without enough knowledge of the subject, but I feel a little concerned about the idea of hanging a language feature off an implementation detail of the subtype checker. Is it very unlikely that the dealiasing strategy you are using now will ever change?

[odersky]

@odersky I'm probably making a foolish-sounding observation without enough knowledge of the subject, but I feel a little concerned about the idea of hanging a language feature off an implementation detail of the subtype checker. Is it very unlikely that the dealiasing strategy you are using now will ever change?

I believe it is very unlikely. But the issue is really broader than that. @adriaanm's version of bringing opaque types to Scala 2 has exactly the same problem, and I showed in my comment that an alternative encoding would also have exactly the same problem. So the problem looks like its fundamental, and the solution for it works in all incarnations, it's just that the self-type encoding hides it bit better than others.

[Blaisorblade]

If we would use one of the encodings of opaque types that does not rely on magic, the dealising would be admissible, but o.T.type would not be recognized as being equal to T.this.type.

This sort of problem is general enough that it appears to be described in the literature. IIUC, this relates to what Derek Dreyer calls this the “double vision” problem, and describes a solution in his RMC and MixML papers.

As far as I understand (not yet much), he uses a first pass to collect the extra type equalities to remember for the actual typechecking pass; that’s what you’re doing here in this special case, essentially, by encoding two upper bounds and two lower bounds into one. It’s not yet clear to me whether this two-pass algorithm is unfeasible for us, or whether we could hack the first pass into namer.

[Blaisorblade]

Here’s a few initial comments on the code.

[Blaisorblade]

Somewhat orthogonal, but having different apparent kinds for the bounds seems surprising? I can see you’re encoding the kind-arity this way.
I expect this fulfills the invariants necessary to Dotty, but those still puzzle me.

[odersky]

Yes, that's still up for reconsideration and a possible change. There's comment in the type lambdas spec that states this.

[Blaisorblade]

tp: TypeOrSymbol (from Types) would be more informative.

[odersky]

Agreed.

[Blaisorblade]

Mmh, wondering if other uses of isStaticOwner need to also test isOpaqueCompanion... TODO check

[odersky]

As far as I understand (not yet much), he uses a first pass to collect the extra type equalities to remember for the actual typechecking pass; that’s what you’re doing here in this special case, essentially, by encoding two upper bounds and two lower bounds into one. It’s not yet clear to me whether this two-pass algorithm is unfeasible for us, or whether we could hack the first pass into namer.

Yes, this looks indeed like an instance of the double vision problem. I believe there's an advantage to solving it without requiring a special pass. And it's kind of cool that union and intersection types allow us to encode multiple aliases in one type. Anyway, Namer is not really a pass, so we could not piggyback operations to it.

[adriaanm]

I'm at Reactive Summit this week, but I'll try to wrap up my review today or tomorrow. I haven't had a chance to solve the "double vision problem" in scalac -- it doesn't carry over directly because we don't have union types, and my naive attempt ran into a illegal cyclic ref problem (thanks @Blaisorblade for the pointer, I hadn't made that connection). For the curious, my wip is at scala/scala@2.13.x...adriaanm:opacity (will submit PR once I figure out that remaining issue)

[odersky]

Another rebase necessary...

[odersky]

I considered an alternative design proposed by @smarter: Instead of the concept of a companion object for opaque types, make the alias visible in the scope where the opaque type is defined, and invisible outside.

This can achieve some simplification, as we do not need to define the concept of a companion object for an opaque type. On the other hand, it risks being less convenient once we allow toplevel opaque types (which would be desirable). Then we run into two problems:

• what is the scope where the opaque type is open? Saying "in the same sourcefile" means adding another concept to the resolution rules.
• what is a good way to add implicits and extension methods to an opaque type? Currently the companion object is ideal since it is in the implicit scope of the opaque type. If we drop that concept, we could still place the conversions in the same class or object where the opaque type is defined. But, again, if the opaque type is toplevel there is no solution.

So, in light of these problems I still think the current spec and implementation is the right one.

[odersky]

@adriaanm Any review comments?

[adriaanm]

A few small things I noticed while reading through. Haven't made it to the docs / examples yet.

[adriaanm]

restore comment?

[odersky]

I had a talk with @smarter about this. The comment is actually misleading, and it's very subtle to argue, first that there could be a problem at all, and, second, why the problem does not arise after all. Also, the condition tpSym.maybeOwner.isType got removed later.

[adriaanm]

Comparing this to scalac's implementation, I noticed we still do ASF post erasure when the prefix is Array || phase.erasedTypes && pre.typeSymbol != ArrayClass. (See val trivial in def asSeenFrom.)

[odersky]

I wonder why?

[adriaanm]

I’ll see if I can find the corresponding bug and report back. I guess erasing a member selection on an array may need to know the element type in the prefix (the array type). Could be that we special cased this elsewhere and this is now redundant.

[adriaanm]

Potentially a premature optimization. It's been in there for about 13 years: scala/scala@2a5f623#diff-2731df2ea3054555efb4a23f8c628acdR158

[adriaanm]

Well, could've been for correctness: that same diff also reworks transformInfo in erasure. These days Array does not extend Seq anymore, so maybe that's why it's redundant?

[adriaanm]

I tried a bootstrap without the special case for Array, but then scalac crashes on compiling ArrayOps.

[odersky]

So, we do compile ArrayOps, so it might be an artifact how parameters are tied to asSeenFrom (which is different in the two compilers).

[allanrenucci]

I tried as well on the 2.13 std lib and it works fine

[adriaanm]

btw, couldn't a term member's info (e.g. a bound) still refer to a member of an outer class?

[odersky]

Sure, but it's already taken care of when the type is constructed.

[LPTK]

@adriaanm From what I understand, the main problem in Haskell is that they have things that behave like type-level functions (type families), which make it unsound to do Liskov-like substitution in general.

I think we do not have the problem in Scala because we don't actually have type-level functions, and instead we use implicit programming, which soundly carries pieces of evidence around... that is, until we introduce match types, which are essentially like closed type families.

Now, we can see why match types introduce unsoundness. Consider:

type M[T] = T match {
  case Int => String
  case O => Bool
}
opaque type O = Int
object O {
  def convert[X[_]]: X[O] => X[Int] = identity
  // ^ inside companion we know O =:= Int
}
case class Oops[A](m: M[A])
val oopsO = Oops[O](true)
val oopsI: Oops[Int] = convert(oops)  // now oopsI.m has type String!
oopsI.m.length  // boom!

The way they solved it in Haskell, IIRC, is using type roles to prevent substitution of types in non-parametric contexts. In Scala, the closest thing would be to have a new type kind that says we can actually interpret X[O] as X[Int] because X is parametric in its parameter.
Another way would be to prevent indexing things on types that rely on 'nominal' equality (as opposed to 'representational'). In our example, we shouldn't be able to index M on O (with the type match) because O has a nominal role.

[odersky]

I was talking to some Haskell people about this, and wanted to understand what they've learned from having newtype in the language. I didn't really manage to understand the problem they were mentioning. The best reference of some challenges (for them) I could find was https://ghc.haskell.org/trac/ghc/wiki/NewtypeWrappers, but I honestly don't really understand how it might relate to potential usages in Scala. (EDIT: papers: https://dl.acm.org/citation.cfm?id=1926411, https://dl.acm.org/citation.cfm?id=2628141)

The Haskell discussion comes from the fact that in Haskell, newtype is defined by means of implicit conversions. The problem is lifting these conversions to types containing newtype occurrences. We don't have that problem since opaque types give rise to equalities, which are true congruences.

One thing that Haskell can do and we can't is the Fix example in SIP 35. Type recursion can be expressed in terms of conversions (i.e. fold/unfold) but not in terms of equalities.

One question I don't know the answer to is how Haskell's approach interacts with type inference. It requires a suitable decomposition of a type into a constructor C and a newtype T. It seems this would need higher-order unification to work in general.

[odersky]

@LPTK Very good example! I believe the way to solve it is to not reduce

M[O] --> Boolean

We already have logic in place for this: When faced with a match type

type M[T] = T match {
  case A => R1
  case B => R2
}

and an occurrence M[U] we are allowed to consider the B case only if it can be ruled out that a substitution instance of U could match A. We have to refine this logic to also consider opaque aliases as real aliases. That should do it.

[odersky]

@ltpk: The match type example is the only one where we consider negative information of the form "A can't possibly be a subtype of B, in all scenarios or substitution instances" to achieve a positive result. I was very nervous about that when first considering this, and your example shows beautifully the traps one can fall into with this.

Haskell has several other such instances (e.g. it's also needed for typeclass coherence), so the problem with type families seems much harder in this setting.

[odersky]

Note that the required logic for match types is not implemented yet (even in the absence of opaque types). I have opened #5417 to track this.

[smarter]

The match type example is the only one where we consider negative information of the form "A can't possibly be a subtype of B, in all scenarios or substitution instances" to achieve a positive result.

I think @Blaisorblade pointed out that GADTs require something similar: #4029

[odersky]

GADT exhaustiveness checking, yes. But that's not such a big deal since these are warnings only.

[abgruszecki]

While we're on the topic of matching: we could use a test case that ensures patmat exhaustivity is aware of opaque types behaviour:

  opaque type Pos = Int

  sealed trait Expr[T]
  final case class PosExpr(p: Pos) extends Expr[Pos]
  final case class IntExpr(i: Int) extends Expr[Int]

  def eval(pe: Expr[Pos]): Pos = pe match {
    case PosExpr(p) => p
    // unexhaustive: IntExpr 
  }

If M[O] only sometimes reduces, then we should also ensure correct behaviour in case like this:

  opaque type NotInt = Int

  type M[A] = A match {
    case Int => String
  }

  sealed trait FunGadt[T, R]
  object StrIntFun extends FunGadt[String, Int]
  object StrStrFun extends FunGadt[M[NotInt], String]

  def get[R](g: FunGadt[M[NotInt], R]): R = g match {
    case StrStrFun => ""
    // unexhaustive: StrIntFun
  }

Finally, as a side note, it might be worth keeping in mind that depending on how match types behave we might be able to match on O by exploiting that M[O] reduces differently from M[Int]

  opaque type O = Int
  type M[A] = A match {
    case Int => String
    case O => Boolean
  }
  type MM[A] = M[A] match {
    case String => String
    case M[O] => Boolean
  }

Which should lead to similar unsoundness as in LTPK's example above. It might be easier to just reduce M[O] the same as M[Int] - at the very least, this follows the intuition that opaque alias is an alias.

[LPTK]

@AleksanderBG

It might be easier to just reduce M[O] the same as M[Int] - at the very least, this follows the intuition that opaque alias is an alias.

Opaque types are just a special case of the general problem of keeping match types sound in the presence of abstract types. You don't always know what an abstract type will end up being an alias to. So you can't always say "it might be easier to just reduce M[O] the same as M[?]". Besides, it would be a failure of abstraction to allow the implementation of an opaque type to leak by way of match types, and would probably cause all kinds of surprises and confusion down the line.

I think the solution, as @odersky explained, is to not reduce matches unless we are certain. We should keep the match type "stuck" as long as we can't be sure that the current case can be ruled out. So in your last example, we can't just skip the case String because we don't know whether M[A] will actually end up being String or not, because we can't rule out that A may be Int (and indeed it is, but we should not be able to observe it).

[Blaisorblade]

It might be easier to just reduce M[O] the same as M[Int] - at the very least, this follows the intuition that opaque alias is an alias.

I agree with @LPTK here, but let me add the rule we should keep in mind.
To be properly hidden, I think opaque types should satisfy some form of separate typechecking: if you change e.g. opaque type O = Int to opaque type O = String, and update the code that can see the definition (the companion object), everything else should typecheck after the change if and only if it typechecks before the change.

If the companion object has externally equivalent behavior, you would also expect the runtime behavior to be the same, by parametricity, except for the known parametricity-breaking escape hatches (e.g. isInstanceOf). It's not clear if type inference should respect this tho.

[abgruszecki]

@Blaisorblade let me show an exception to your rule:

opaque type Pos = Int
object Pos {
  def mkPos(i: Int): Pos = {
    require(i > 0)
    i
  }
  def coerce[F[_]](fa: F[Int]): F[Pos] = fa
}

sealed trait Expr[T]
final case class PosExpr(p: Pos) extends Expr[Pos]
final case class IntExpr(i: Int) extends Expr[Int]

def eval(e: Expr[Pos]): Pos = e match {
  case PosExpr(p) => p
  case IntExpr(_) => Pos.mkPos(1)
}

eval(Pos.coerce[Expr](IntExpr(-1)))

(EDIT: fixed the issue from the comment below)
This typechecks as long as Pos = Int (and indeed is necessary to compile without warnings), but breaks if we say Pos = String (IntExpr is no longer a valid pattern for Expr[Pos]). Consider the last line to see why we need to allow IntExpr as a pattern for Expr[Pos], and why we should emit an inexhaustive match warning if IntExpr would be missing.

One way or another, we will have to leak that opaque types do not create a proper new type.

EDIT: Let me maybe say something more to clarify the difference between newtypes and this implementation of opaque types: newtypes truly create a new type, isomorphic to the old one but never equal to it. The isomorphism can then be exploited to zero-cost coerce between two types that share the same runtime representation (for Scala, this would mean that we'd be able to coerce Pos <=> Int, List[Pos] <=> List[Int], but not Expr[Pos] <=> Expr[Int]).

In contrast, Scala opaque types simply create a type alias which is hidden from most of typechecking. In particular, we can convert between Expr[Pos] and Expr[Int], becase Pos is ultimately just an alias and not a separate type from Int.

To complete the picture, Haskell coerce has the following signature:

coerce :: Coercible a b => a -> b

Coercible is a magik typeclass which is synthesized by the compiler and cannot be directly created by users. One magik thing about it is that it is actually allowed to be incoherent and special-cased as such by GHC [1]. The rules for deriving Coercible are such that we can derive Coercible [Pos] [Int], but not Coercible (Expr Pos) (Expr Int). Finally, if I understand everything correctly, the deriving mechanism for Coercible allows them to avoid higher-order unification problems (as opposed to signature like coerce :: f a -> f b).

[1] - https://dl.acm.org/citation.cfm?id=2628141

[sjrd]

This typechecks as long as Pos = Int

No it doesn't: i of type Int cannot be assigned to a Pos.

[odersky]

I want to talk about Opaque types on Wednesday at Scale by the Bay. So it would help if this was merged by then.

[adriaanm]

@AleksanderBG the equality Pos = Int is only visible inside the companion object of the opaque type. I wouldn't expect your example to type check outside of it.

[adriaanm]

@odersky this PR seems good to go, but I'd like to keep the discussion regarding feature interaction with match types / GADTs / ... going somewhere. What would be the right place for that?

[odersky]

@adriaanm #5417 is an open issue where we collect topics and TODOs that affect match types.

[Blaisorblade]

• We realized today that opaque types are replaced by their definition pretty early, breaking abstraction in a number of cases. However, for some warnings, @odersky argues it makes sense to see through opaque aliases. I think those should be the exception not the rule, if such valid examples exist.

He mentioned warnings redundant match warnings, but thinking about it I am not sure what the example would be, as all the examples I can write seem illegal:

def eval(e: Pos) = e match {
  case x: Pos => // illegal; if it were allowed, next case would be redundant.
  case x: Int =>
}

• About the interaction with GADTs, I answered (with a summary of today's examples) in WIP: Constraint-based GADT reasoning #5258 (comment). I expect that example is currently broken since opaque types are dealiased before the PatternMatcher phase.

[odersky]

I am merging this now. We should evaluate separately whether we want to move the ElimOpaque phase later. Right now it looks like this:

         new RefChecks) ::           // Various checks mostly related to abstract members and overriding
    List(new ElimOpaque,             // Turn opaque into normal aliases
         new TryCatchPatterns,       // Compile cases in try/catch
         new PatternMatcher,         // Compile pattern matches
         new ExplicitOuter,          // Add accessors to outer classes from nested ones.
         new ExplicitSelf,           // Make references to non-trivial self types explicit as casts

It would take probably not take much to move it after PatternMatcher but at this stage I am not sure that we should do it. It's best to do these deliberations separately.