Fixes and improvements to erasure #11695

odersky · 2021-03-10T19:19:08Z

make erasedTerms a language import
drop -YerasedTerms setting
make erased a soft modifier
fix bugs in erasure involving context functions
allow erased on classes as well
explain erased classes in docs

nicolasstucki · 2021-03-12T08:30:21Z

Currently erased only defined semantics on terms. What would be the semantics of an erased class? What is the use-case?

My intuition is that it would serve a similar purpose as a Phantom type, but in that case I would start with erased type. Any instance of such type must be erased.

Another one that might be useful if the erased object. This would serve as a place to define erased given without generating the object at runtime. It might even be possible to add non-retained inline def in such a object.

japgolly · 2021-03-12T09:56:12Z

What would be the semantics of an erased class? What is the use-case?

An opinion from the sidelines: I would love to use this to define compile-time-only proofs. Having some kind of proof be an erased class would give me confidence that it's guaranteed to be erased and that it can't accidentally be misused in a way that it's instantiated at runtime. My understanding is that without the class itself being marked as erased, the onus is on me (or downstream users) to always ensure we don't accidentally forget to declare a given/function-arg/whatever as erased. That would get pretty tedious pretty quickly in large code bases.

Question: if an erased class is used without being marked as such (eg. given instead of erased given), would it be

a compilation error (eg. `hey! you need to change "given" to "erased given")
or could the compiler automatically mark the given as erased too?

As a user, I think (2) would be awesome 😄

japgolly · 2021-03-12T10:04:04Z

Btw this would be one of my first use-cases for this awesome feature: universal equality proof at compile-time guaranteed to always just translate to x == y after compilation.

erased final class UnivEq[A]:
  inline def univEq(a: A, b: A): Boolean =
    a == b

I'm currently in the process of defining it like this for Scala 3 without an erased class:

// Declaring in a different package because inline methods aren't allowed in opaque types companions :(
package internal:
  opaque type UnivEq[A] = Unit

  object UnivEq:
    def force[A]: UnivEq[A] =
      ()

type UnivEq[A] = internal.UnivEq[A]

object UnivEq:

  inline def force[A]: UnivEq[A] =
    internal.UnivEq.force

  extension [A](proof: UnivEq[A])
    inline def univEq(a: A, b: A): Boolean =
      a == b

Then of course there are extension method ops but you get the idea.

https://github.com/japgolly/univeq

odersky · 2021-03-12T10:30:06Z

As a user, I think (2) would be awesome 😄

So you'll be happy to know that that's what's implemented!

odersky · 2021-03-12T12:45:14Z

Btw, I tried to make the import

import language.experimental.erased

but that failed the bootstrap since erased is a hard keyword under -Yerased-terms. Maybe once -Yerased-terms is gone we can do that change.

japgolly · 2021-03-12T21:15:46Z

So you'll be happy to know that that's what's implemented!

Oh wow @odersky that is fantastic news!! ❤️

japgolly · 2021-03-12T21:18:07Z

In case you hadn't thought of it yet, =:= and <:< seem like ideal first uses from Scala stdlib.

odersky · 2021-03-12T22:50:38Z

In case you hadn't thought of it yet, =:= and <:< seem like ideal first uses from Scala stdlib.

Yes, once we get a chance to change it.

nicolasstucki

In case you hadn't thought of it yet, =:= and <:< seem like ideal first uses from Scala stdlib.

That is one of the oldest usecases we have (see old gist). But we need to be able to break the binary compatibility of the standard library to make this change. Note that to implement this we do not need erased classes unless we try to naively port the old implementation. Here is how one would start implementing it.

type <::<[-From, +To]
type =::=[From, To] <: (From <::< To)
erased given [X]: (X =::= X) = scala.compiletime.erasedValue
extension [From](x: From)
  inline def cast[To](using From <::< To): To = x.asInstanceOf[To] // Safe cast because we know `From <:< To`

nicolasstucki · 2021-03-15T09:05:32Z

compiler/src/dotty/tools/dotc/config/Feature.scala

-  private val symbolLiterals: TermName = deprecated("symbolLiterals")
+  private val namedTypeArguments = experimental("namedTypeArguments")
+  private val genericNumberLiterals = experimental("genericNumberLiterals")
+  private val macros = experimental("macros")


Suggested change

private val macros = experimental("macros")

private val scala2macros = experimental("macros")

We also use the name macros for Scala 3 macros in the compiler.

nicolasstucki

We should split this PR into 2

Make erased an experimental language feature
Add new erased class, find use cases where it is needed and make sure it is sound (phantom types?)

nicolasstucki · 2021-03-15T09:27:59Z

compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala

@@ -925,7 +925,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
      else PrintableFlags(isType)
    if (homogenizedView && mods.flags.isTypeFlags) flagMask &~= GivenOrImplicit // drop implicit/given from classes
    val rawFlags = if (sym.exists) sym.flags else mods.flags
-    if (rawFlags.is(Param)) flagMask = flagMask &~ Given
+    if (rawFlags.is(Param)) flagMask = flagMask &~ Given &~ Erased


We might also want to remove Inline

No, inline is per param, not per clause

nicolasstucki · 2021-03-15T09:35:42Z

docs/docs/reference/metaprogramming/erased-terms-spec.md

   * At the start of a parameter block of a method, function or class
   * In a method definition
   * In a `val` definition (but not `lazy val` or `var`)
+   * In a `class` or `trait` definition


If we have class and trait we should also have object. Maybe for later.

It can be emulated with the following code

type Foo erased val Foo: FooModule = erasedValue erased trait FooModule: /*erased*/ given Foo = erasedValue

Right now I'd only do the minimum we need. Instead of erased object you can always write erased val.

nicolasstucki · 2021-03-15T09:47:54Z

docs/docs/reference/metaprogramming/erased-terms.md

+## Erased Classes
+
+`erased` can also be used as a modifier for a class. An erased class is intended to be used only in erased definitions. If the type of a val definition or parameter is
+a (possibly aliased, refined, or instantiated) erased class, the definition is assumed to be `erased` itself. Likewise, a method with an erased class return type is assumed to be `erased` itself. Since given instances expand to vals and defs, they are also assumed to be erased if the type they produce is an erased class. Finally


a method with an erased class return type is assumed to be erased itself

This should not be that case. This looks suspiciously like a rule from the old Phantom types. Return types should not affect the erasedness of a definition. It should behave as an abstract type would.

The restrictions come from the fact that if a method returns an instance of an erased class they must either make the definition erased or they will not be able to instantiate the class as it can only be instantiated.

If we allow this rule we would effectively be reintroducing some form of phantom type. But with fewer guarantees than the original phantom type. This sounds like a potential source of unsoundness that we would need to check in detail.

I disagree. If val x: CanThrow becomes erased val x: CanThrow then def x: CanThrow should also become erased def x: CanThrow, and def x(): CanThrow should become erased def x(): CanThrow.

I don't think there's a soundness issue since these are purely syntactic conventions, akin to simple desugarings.

nicolasstucki · 2021-03-15T09:59:55Z

tests/neg/safeThrowsStrawman.scala

+
+object scalax:
+  @implicitNotFound("The capability to throw exception ${E} is missing.\nThe capability can be provided by one of the following:\n - A using clause `(using CanThrow[${E}])`\n - A throws clause in a result type such as `X throws ${E}`\n - an enclosing `try` that catches ${E}")
+  erased class CanThrow[-E <: Exception]


Suggested change

erased class CanThrow[-E <: Exception]

type CanThrow[-E <: Exception]

there is no point in having the ability to instantiate instances of CanThrow if the only places where we will create them is in

erased given CanThrow[Fail] = erasedValue

Making it a type makes it simpler for users by removing ways they could miss-use this abstraction. It will also compile faster.

Classes are sticky, types are not. That's why we use a class for erased.

nicolasstucki · 2021-03-15T10:01:56Z

tests/neg/safeThrowsStrawman2.scala

+
+object scalax:
+  erased class CanThrow[E <: Exception]
+  type CTF = CanThrow[Fail]


Why not?

type CanThrow[E <: Exception] type CTF = CanThrow[Fail]

nicolasstucki · 2021-03-15T10:19:37Z

@japgolly

I'm currently in the process of defining it like this for Scala 3 without an erased class:

// Declaring in a different package because inline methods aren't allowed in opaque types companions :(
package internal:
  opaque type UnivEq[A] = Unit

  object UnivEq:
    def force[A]: UnivEq[A] =
      ()

type UnivEq[A] = internal.UnivEq[A]

object UnivEq:

  inline def force[A]: UnivEq[A] =
    internal.UnivEq.force

  extension [A](proof: UnivEq[A])
    inline def univEq(a: A, b: A): Boolean =
      a == b

It seems like this code can simply be translated to erased types as

type UnivEq[A]
object UnivEq:
  erased def force[A]: UnivEq[A] = erasedValue
  extension [A](erased proof: UnivEq[A])
    inline def univEq(a: A, b: A): Boolean =
      a == b

Issue: we cannot have extensions method on erased types (see #11743)

P.S.
Adding methods to this version of UnivEq is an antipatern if it is intended to be used as given instances. Adding methods forces the using instances to be named or the use of summon in the usercode. The alternative is to write static methods instead.

type UnivEq[A]
object UnivEq:
  erased def force[A]: UnivEq[A] = erasedValue
  inline def eq(a: A, b: A)(using erased UnivEq[A]): Boolean = a == b

nicolasstucki · 2021-03-15T10:21:14Z

It seems we do not have any use case for erased class assuming that #11743 is fixed.

nicolasstucki · 2021-03-15T10:31:35Z

Note: There is a pattern that I have seen since the early days of phantom type. Whenever we try to port a class that should be phantom types, if we try to emulate the original definitions as a class we always end up with awkward and useless code. On the other hand, when we simply started by defining the type and type Foo[X] and added the functionality on to of it the code ended up simpler, shorter and easier to understand.

nicolasstucki · 2021-03-15T10:39:59Z

In the current verison of erased class we are mixing two distinct features.

Make all members erased (as shorthand for withing type with extension methods on erased self / workaround Support extension methods on erased types #11743)
Make the type a phantom type (allow inference of erasedness of definitions based on type)

We also accidentally make the type a subtype of AnyRef. This is not a desirable property of a phantom type.

If we what to add phantom type we should start from erased type which would have more usecases.

nicolasstucki · 2021-03-15T15:19:14Z

This is failing

erased class A
erased class B extends A

could not translate

type <::<[-From, +To]
type =::=[From, To] extends <::<[From, To]

odersky · 2021-03-16T11:22:21Z

I think the presumed similarity with phantom types is misleading. This is something completely different, with different rules.

nicolasstucki · 2021-03-16T12:10:17Z

Now that I understand what it does, the misleading part is that erased class does not define a class but only the type. There must be a way to make this distinction clearer.

My current understanding is that an erased class defines a type and that any type that derives from will also be an erased type. Then if a term has an erased type it automatically becomes erased. Is that description complete?

nicolasstucki · 2021-03-16T12:24:59Z

Inference of erasedness of parameters does not seem to be working

import scala.language.experimental.erasedTerms

erased class ErasedTerm

type <::<[-From, +To] <: ErasedTerm

type =::=[From, To] <: (From <::< To)

erased given [X]: (X =::= X) = scala.compiletime.erasedValue

extension [From](x: From)
  inline def cast[To](using From <::< To): To = x.asInstanceOf[To] // Safe cast because we know `From <:< To`


def convert[A, B](a: A)(using /*erased*/ x: A <::< B): B =
  // println(x) // error: OK because x should be erased
                // but currently x is not marked as erased which it should
  a.cast[B]


@main def App: Unit = convert[Int, Int](3) // should not be an error

odersky · 2021-03-16T17:16:45Z

Inference of erasedness of parameters does not seem to be working

That's because types don't generate erased vals; only erased classes do this. And types themselves cannot be erased.

nicolasstucki · 2021-03-16T17:28:25Z

Then how do we abstract over capabilities? I would have expected the following to work but I guess it won't

erased class Capability

def foo[Cap <: Capability](using c: Cap): T = ...

Is c erased or not? Given the previous rule it seams not. But the only values we can create for it are erased.

I remember that this kind of code appeared with some utility functions for capabilities bit I can't remember which one at the moment.

nicolasstucki · 2021-03-16T17:32:01Z

Are CanThrow[X] & CanThrow[Y] and CanThrow[X] | CanThrow[Y] erased?

odersky · 2021-03-16T17:40:04Z

My current understanding is that an erased class defines a type

Yes, in a trivial sense, like any other class.

and that any type that derives from will also be an erased type.

No.

Then if a term has an erased type it automatically becomes erased. Is that description complete?

True only if you replace type by class. type definitions cannot be erased.

odersky · 2021-03-16T18:06:20Z

Type parameters and union / intersection types are never erased. It's just class references as the docs state.

The whole thing is just a syntactic convenience, and we want to keep it simple. Maybe we can extend it in the future if use cases demand it.

nicolasstucki · 2021-03-17T15:32:37Z

compiler/src/dotty/tools/dotc/config/Feature.scala

@@ -24,7 +24,7 @@ object Feature:
  private val scala2macros = experimental("macros")

  val dependent = experimental("dependent")
-  val erasedTerms = experimental("erasedTerms")
+  val erasedDefinitions = experimental("erasedDefinitions")


Erased is not only about definitions. It is also about the term values they provide. This is completely lost with this new name. The erased class concept is also about erasing term definitions and uses as arguments. Therefore, the scope of the feature has not really changed.

But erased is a modifier on a definition, not a term. Anyway, people usually do not know what a term is. We'd have to say erasedExpressions, but I believe Definitions is preferable, since that's where the erased goes.

The fact that if you erase a definition you also erase its RHS, and if you erase a parameter, you also erase its argument follows naturally since it's the only thing that makes sense. But the trigger is the erased on a definition. Or parameter, but I think it's OK to include that in the meaning.

…liub build

Map erased classes to empty interfaces.

odersky force-pushed the add-safe-throws branch from 7f69dc4 to e9c944d Compare March 11, 2021 12:57

nicolasstucki self-requested a review March 11, 2021 16:59

odersky force-pushed the add-safe-throws branch from 0289612 to c616203 Compare March 11, 2021 17:54

odersky marked this pull request as ready for review March 12, 2021 12:43

odersky assigned nicolasstucki Mar 12, 2021

odersky mentioned this pull request Mar 12, 2021

Safer exceptions #11721

Merged

nicolasstucki reviewed Mar 15, 2021

View reviewed changes

nicolasstucki suggested changes Mar 15, 2021

View reviewed changes

nicolasstucki mentioned this pull request Mar 15, 2021

Support extension methods on erased types #11743

Closed

odersky force-pushed the add-safe-throws branch 2 times, most recently from eaae050 to ef0341b Compare March 17, 2021 13:36

nicolasstucki suggested changes Mar 17, 2021

View reviewed changes

odersky assigned nicolasstucki and unassigned odersky Mar 17, 2021

odersky added 19 commits March 17, 2021 18:58

Streamline feature handling in Parser

0d70a4a

Add language import for erasedTerms

0d48ba0

Fix problem when erasing erased context functions

513e95d

Eliminate -YerasedTerms

f9ffafd

Bring back -Yerased-terms for bootstrapping

6944fc6

Fixes for turning erased into a soft modifier

53793ae

Allow erased on classes

5a62261

Check that no references to erased classes survive

8c42294

Explain erased classes in doc page

1223ea2

Make tests variance aware

7c4e3a9

Replace -Yerased-terms with -language:experimental.erasedTerms in std…

310d87e

…liub build

Update check file

07a47f1

Rename macros feature to scala2macros

313221a

Also erase methods with erased class results

799f6e4

Semi-erase classes

1558591

Map erased classes to empty interfaces.

Another test

d4e477c

Allow erased as extension parameter

d2b2ddd

Rename erasedTerms language import to erasedDefinitions

f946c4b

Update stdlib to erasedDefinitions language import

0af3f59

odersky force-pushed the add-safe-throws branch from ef0341b to 0af3f59 Compare March 17, 2021 17:59

nicolasstucki approved these changes Mar 18, 2021

View reviewed changes

nicolasstucki merged commit 422ffbc into scala:master Mar 18, 2021

nicolasstucki deleted the add-safe-throws branch March 18, 2021 08:39

Kordyjan modified the milestones: 3.0.0-RC2, 3.0.0 Aug 2, 2023

	private val macros = experimental("macros")
	private val scala2macros = experimental("macros")

	erased class CanThrow[-E <: Exception]
	type CanThrow[-E <: Exception]

Fixes and improvements to erasure #11695

Fixes and improvements to erasure #11695

Conversation

odersky commented Mar 10, 2021 • edited Loading

nicolasstucki commented Mar 12, 2021

japgolly commented Mar 12, 2021

japgolly commented Mar 12, 2021

odersky commented Mar 12, 2021

odersky commented Mar 12, 2021

japgolly commented Mar 12, 2021

japgolly commented Mar 12, 2021

odersky commented Mar 12, 2021

nicolasstucki left a comment • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nicolasstucki left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky Mar 16, 2021 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nicolasstucki commented Mar 15, 2021 • edited Loading

nicolasstucki commented Mar 15, 2021

nicolasstucki commented Mar 15, 2021

nicolasstucki commented Mar 15, 2021

nicolasstucki commented Mar 15, 2021 • edited Loading

odersky commented Mar 16, 2021

nicolasstucki commented Mar 16, 2021

nicolasstucki commented Mar 16, 2021

odersky commented Mar 16, 2021

nicolasstucki commented Mar 16, 2021

nicolasstucki commented Mar 16, 2021

odersky commented Mar 16, 2021

odersky commented Mar 16, 2021

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky commented Mar 10, 2021 •

edited

Loading

nicolasstucki left a comment •

edited

Loading

odersky Mar 16, 2021 •

edited

Loading

nicolasstucki commented Mar 15, 2021 •

edited

Loading

nicolasstucki commented Mar 15, 2021 •

edited

Loading