Pre SIP: Replace non-sensical @unchecked annotations

[Sporarum]

I think this is a very well thought of proposal, and I support it, it also has the benefit of allowing more documentation !
Since we now have a method and a type, we can clearly explain what each does, and what happens when you use them

[sjrd]

@alvae and @lihaoyi have already articulated quite well many reasons why checkedCast as a method that returns : x.type does not behave like a method. I won’t repeat that here.

I just want to reply to two concrete comments:

@odersky

“most intents and purposes” means no target typing. But target typing is a fact in Scala and many other languages. Implicit conversions would not work without it and half of type inference would not work without it either. The only difference between standard target typing and checkedCast is that we now also assume that the target type gives information about refutable patterns and inexhaustive matches. That’s an easy and natural generalization step in a situation where we want to convert these faults from runtime errors or warnings to static errors. Rejecting this analogy and elevating it to a fundamental difference is what I am continuously calling “hair-splitting”.

Target typing cannot explain what is proposed here.

Until now, target typing can always be explained away as desugaring during typechecking. After typechecking (after elaboration to be precise), the behavior of a program can be fully explained without target typing. For asInstanceOf in particular, it did receive an actual type parameter, and that type parameter will not change anymore. If we move it and assign it to a separate val (for example, in a macro or compiler phase), it will keep that concrete type parameter.

With the proposed behavior of checkedCast, and if it wants to be explained in terms of target typing, this assumption is broken. Even in a macro or a compiler phase, you are not allowed to extract the call in a separate val, as it will cause compile errors that would not be there otherwise. This illustrates that the Match(Apply(_, checkedCast), ...) is magical as a pair of syntactically nested nodes.

This is not hair splitting. It has very concrete consequences that will break people’s code.

Take for example a macro for async/await. Such a macro typically needs to perform some sort of ANF transform, which does mean extracting subexpressions and putting them into vals. The macro would be well-behaved, well-tested, on every possible Tree of the metaprogramming API. And then when a user happens to use x.checkedCast match inside async { ... }, bam! they get a compile error that makes no sense.

To fix that, the macro author will have to add a specific case for Match(Apply(x, checkedCast), ...) in order not to extract that Apply. How do we expect a macro author to know that? Or to think about testing that particular combination of features? We cannot. Macros will get broken, and it won’t the macro authors’ fault; it will be our own, for designing an elaborated form of the language that is not compositional.

@bishabosha

so therefore

def myChecked[T](t: T): t.type = t.checkedCast

is “desugared” to

def myChecked[T](t: T): t.type = t match
  case t0: t.type => t0
  case _ => ???

which is a no-op and therefore checkedCast behaves like a method, can we move on

This can only explain the cases where a better type is enough to guarantee exhaustivity checking. But the original proposal definitely wants to be able to do things like

val Foo(Bar(x)) = any.checkedCast

or

val List(one, two) = list.checkedCast

which cannot be explained that way. So no, that does not work and we cannot move on

If we could, then my suggestion from way earlier to give a simple, user-land definition of .checkedCast would have sufficed. As a reminder, it looked like:

extension [S] (x: S) def checkedCast[T](using TypeTest[S, T]): T = x match
  case x: T => x
  case _    => throw MatchError(x)

That one would have been completely explained by target typing as we know it today. Not just the signature but even the implementation!

[bishabosha]

@sjrd

This can only explain the cases where a better type is enough to guarantee exhaustivity checking. But the original proposal definitely wants to be able to do things like

val Foo(Bar(x)) = any.checkedCast

or

val List(one, two) = list.checkedCast

which cannot be explained that way. So no, that does not work and we cannot move on

the original proposal also mentions

@odersky

This is typically if the expected type of the asInstanceOf is underdefined. By contrast, an underdefined expected type would lead to a warning or error in the match expansion of checkedCast.

which I took to mean if a valid type that would silence warnings can be extracted, then it will become that type. e.g. ::[Any] can come from List[Any], but not ::[Int], as Int is again unchecked

[Ichoran]

@lihaoyi

1. checkedCast is defined in the standard library as below (it could also be an extension method or static method)

trait Any{ 
  def checkedCast: CheckedCast[this.type] = this.asInstanceOf[CheckedCast[this.type]] 
}

2. scala.CheckedCast[T] is a “magic” opaque type alias defined in the standard lib

opaque type CheckedCast[T] = T

3. scala.CheckedCast[T] is handled specially by the compiler.

I had these features in my proposal too (hidden in a scastie link), but with one key difference; [T] is not the type of what you were but rather what you want to become. You explicitly lose track of what you were.

extension [A](any: A)
  inline def checkedCast[T]: CheckedCast[T] = any

At that point I think it fills all the requirements: a little magic on how to fill in [T] and how you match against CheckedCast[T]–mostly acting as if there is a Conversion[CheckedCast[T], T] in scope–and you’re good.

[nafg]

I’m still confused what casting has to do with exhaustivity checking.

(Also, I’d like to know more about when and to what extent patterns affect the expected type, for target typing to be relevant. I didn’t know it could affect it at all if the patterns are part of a match.)

[arturopala]

@odersky

  val x: Any = ???
  val (y: Int) = x: @unchecked // works
  val y: Int = x: @unchecked

what about writing this as:

val x: Any = ???
case val (y: Int) = x
case val y: Int = x

or

val x: Any = ???
val case (y: Int) = x
val case y: Int = x

[odersky]

I could live with that proposal, even though I am not convinced the added complication is necessary. checkedCast as a simple method works perfectly well IMO. But if others feel we have to reify this as a type, I could go along with it.

Just as a counter-point: We use implicit conversions (user- or system-defined) all the time, and yet nobody so far has proposed “being convertible” should be reified into a type. So I think it’s a bit of overkill to do so for CheckedCast, but it’s certainly better than the status quo.

It does not even have to be implicit conversions. For instance here is a very nice method that
makes conversions explicit:

extension [A](x: A) def convert[B](using Conversion[A, B]): B

Now, you write

x.convert

indicating that an implicit conversion will kick in at this point which depends on the target type. In my opinion, as far as the user is concerned, x.checkedCast is very similar to this. The technical argument against is that unlike convert, checkedCast cannot be given a type signature, But adding CheckedCast as a magical type only shifts the problem around and complicates it further.

[Ichoran]

@odersky

nobody so far has proposed “being convertible” should be reified into a type

That’s because the reification is done by a given Conversion being in scope. I like that much better than the old completely-non-explicit way of doing things.

I’m fine with a similar type-witness to the checked-castedness of a particular thing; I just think the ergonomics would be poor considering how it’s usually used.

given CheckedCast[xs.type] = ???
val y :: ys = xs

So while I love the explicit conversions method you wrote (.convert is basically Rust .into()), to me this argues in favor of the same kind of explicitness you get with Conversion for checkedCast as well, which most easily would be solved by giving it an explicit type.

I still think the name could use some bikeshedding. What we’re actually doing is trusting at compile-time that the cast is valid, even though the type suggests that it’s not, but verifying at runtime.

// Not an actual suggestion
val y :: ys = trustButVerify{ xs }

Maybe something about trusting or runtimeVerify or somesuch would capture the intent and mechanism enough better so that people could use it with only minimal training. If you read checkedCast and you don’t know what it means, you don’t have much chance of figuring it out on your own. But something along the trust/verify lines might be self-evident enough.

[odersky]

We had a brief discussion about this at the last SIP meeting. An important point that emerged from that is that we want to distinguish the source syntax from its elaboration. Dot syntax is convenient as source syntax, but if it translates to a method call, all meta programming has to treat this call specially, which is problematic.

Moreover, if we accept source syntax is different from elaboration, we don’t need to change the language proper at all. The following trick, suggested by @bishabosha, works:

  extension [A](x: A)
    transparent inline def checkedCast: x.type = x: @unchecked

  val xs = List(1, 2, 3)

  val z :: zs = xs.checkedCast

  xs.checkedCast match
    case y :: ys =>

So that means we can drastically cut down on the size of the suggested changes. I suggest we just do the following:

1. Deprecate @unchecked in the role it is used here and replace it by a more sensical name. As I have argued at the start of this thread @unchecked is bad since it is used in two different places, one where it genuinely means “unchecked” (on type parameters in patterns) and the one here where it means “checked at runtime” and is used to suppress exhaustivity or refutability warnings. So I propose to introduce a new annotation named @checkedCast that replaces unchecked in the second role.

2. Add the checkedCast method above to Predef, adjusted so that it uses the @checkedcast annotation instead of @unchecked (we can do that in Scala 3 without waiting for the standard library to thaw).

The @checkedCast annotation could be defined in annotation.internal to avoid two ways of expressing the same thing.

[bjornregnell]

I think this sounds like a very good solution, and also a less “intrusive” change compared to changing the language!

I’d prefer if the name indicated something about that the check is made at runtime; I agree with @Ichoran that the name checkedCast is not that obvious in what it does, just from reading it the first time, without looking up docs, and the intention is to move the check from compiletime to runtime, and I think the name should reflect the intention and be comprehensible at a first-time read by new-comer to Scala.

[odersky]

I think any replacement for checkedCast should not be longer than that, since checkedCast is already quite long.

[matthew.rooney]

I quite like the typescript syntax of ! for this isn’t null or undefined (although that would probably play havok with akka etc). Not helpful I know but perhaps there is a short an sweet symbol which can be used

[bjornregnell]

I’d prefer not using a symbol as it is cryptic/esoteric to beginner/seldom-users. So something short but with letters that says something about the intention.

[bjornregnell]

Yes, short is good. And maybe the shorter checked is better and less esoteric compared to checkedCast as the term “cast” might be unknown by the reader (we don’t even use that term in the method name when using asInstanceOf[T])

But I think it might be worth spending some more letters and go for runtimeChecked as it says what it does (c.f. the explanation in you original post where you describe it as “checked at runtime”). I guess this is not a very commonly used or normal thing to do, comparing to asInstanceOf[...] that is also quite long but OK as it is unusual.

scala> "checkedCast".size
val res9: Int = 11
                                                                                
scala> "runtimeChecked".size
val res10: Int = 14

[jducoeur]

If we’re counting characters – my instinct here was the same as @bjornregnell’s, but I landed on .runtimeCheck, which comes across slightly more as an imperative command than a statement. (Which I think is correct for the sense of what’s happening.)

But yeah: IMO it’s extremely helpful to spell out the “runtime” part of this, which makes it much clearer what’s going on.

And I also agree that I’m not that concerned about length: in practice, this is a tool I reach for relatively rarely, so I’d much rather it be glanceably clear than short.

[bjornregnell]

Yeah after tasting it for a while I also like the imperative nature and its saving of two chars:

scala> "runtimeCheck".length
val res11: Int = 12

[rssh]

runtimeCast

?
(11)

[bjornregnell]

It’s shorter! However, there is a check at runtime and then, if it is followed by a match, there might be a cast as in type pattern, but the main thing with this new extension method is postponing the check until runtime so I prefer runtimeCheck over runtimeCast, and I think the term cast maybe is not that obvious to users who are not so seasoned in imperative OO lingo.

[bishabosha]

I think that given that the method makes a value “runtime checkable” (i.e the actual check is still delayed until the match) perhaps we should reuse the same terminology - asRuntimeCheckable, we already have asMatchable too.

Actually, why can’t we repurpose asMatchable for this? it is intended to enable recovering the runtime type of Any

[bjornregnell]

I like the correspondance of the leading “as” as in “asInstanceOf”, but as @odersky pointed out it is rather long (18 chars).

Here is a summary of proposals so far (did I forget any?):

• checked
• checkedCast
• checkedAtRuntime
• runtimeChecked
• runtimeCheck
• runtimeCast
• asRuntimeCheckable

I think I want runtimeCheck even if I also like the last one starting with as.