Pre SIP: Replace non-sensical @unchecked annotations

[aboisvert]

I’m wondering if we could apply the magic method on match itself, something like match.? and then use the same syntax for val definition patterns, like [pattern].?

Examples:

x match.?
  case Some(value) =>
  case Some(other) =>

and

val ArraySeq(x, y).? = string.split(",")

[odersky]

I think I’ll go ahead and file a SIP with checked (or maybe checkedCast) as an extension method on the scrutinee of a match / right hand side of a val.

[som-snytt]

x.✓ match case 42 =>

I would argue that it exploits the semantic ambiguity of “check”.

It is common in Swedish schools for a ✓ to indicate that an answer is incorrect, while “R”, from the Swedish rätt, i.e., “correct”, is used to indicate that an answer is correct.

In Finnish, ✓ stands for väärin, i.e., “wrong”, due to its similarity to a slanted v. The opposite, “correct”, is marked with

In American schools, of course, the check mark merely means that the teacher or TA checked that the student turned in some work, not that anyone read the answer for correctness. As soon as you assign a grade or mark, you’re barraged with pleas for partial credit, so it’s safer to be non-committal.

[Sporarum]

I completely agree that @unchecked is not good, and should be replaced

What I don’t understand is why it can’t be just another annotation ?

If the syntax currently doesn’t allow it, can we for example allow annotations on matches ?

foo match @runtime
  case ...

[nafg]

@odersky

I think the argument against using a method have to do with the name. xs.unsafe is indeed weird. In what sense is xs unsafe? But xs.checked or xs.checkedCast is perfectly good, since it is xs that is checked at runtime against the expected pattern(s).

I strongly disagree. We need syntax to influence what the compiler does, but it is an major violation of the principle of least surprise to make that syntax look like a method. It has nothing to do with naming, although I agree the naming is important too. I don’t think checked is any better, and checkedCast is only slightly less ambiguous. But this is not about the name at all.

Besides it violates locality – I’d call it spooky action at a distance. Scala is elegant because it avoids that sort of thing, like static members in other languages.

I would say either the very syntax itself whose behavior is being changed has to be different (whether by replacing the = with something else or by surrounding the pattern with something, perhaps curly braces), or else we need some kind of “strict mode” like some languages have.

• In javascript you put "use strict"; in a file or method
• In Typescript it’s a setting in the standard JSON config file

Perhaps a language import or flag would be the Scala equivalent of those?

Also, when I asked ChatGPT about “strict mode in various programming languages” its answer mentioned that “Ruby has a command line option -w or -W to set the warning level, which can be used to enforce a kind of strict mode,” which makes me wonder if this can be achieved via -Wconf / @nowarn.

(YouChat also pointed out that bash set options can be thought of as strict modes)

Alternatively if we want to have special syntax for strict or lenient modes it could be some kind of block like strict { ... } or unsafe { ... }

[odersky]

@nafg

I strongly disagree. We need syntax to influence what the compiler does, but it is an major violation of the principle of least surprise to make that syntax look like a method. It has nothing to do with naming, although I agree the naming is important too. I don’t think checked is any better, and checkedCast is only slightly less ambiguous. But this is not about the name at all.

There are precedents for magic methods. isInstanceOf, asInstanceOf, eq, ne, and so on. Scala’s philosophy is unification, not splitting hairs. Example: Java invents new syntax for assert, because it is special. We use a method. Almost all other languages use [ _ ] for array indexing. For us these are just function calls. And so on. The whole point of Scala is to be simple and easy to use by unifying things, starting with objects and methods.

@nafg

Besides it violates locality – I’d call it spooky action at a distance. Scala is elegant because it avoids that sort of thing, like static members in other languages.

Exactly the opposite is true. We are very precise where we need the checked cast here. By contrast, a language import or compiler setting is spooky action at a distance.

[lihaoyi]

@odersky

There are precedents for magic methods. isInstanceOf, asInstanceOf, eq, ne, and so on. Scala’s philosophy is unification, not splitting hairs. Example: Java invents new syntax for assert, because it is special. We use a method. Almost all other languages use [ _ ] for array indexing. For us these are just function calls. And so on. The whole point of Scala is to be simple and easy to use by unifying things, starting with objects and methods.

One big difference here is that isInstanceOf, asInstanceOf, eq, ne, Array#apply, etc. are all “well behaved”: You can describe them fully in the type system, can assign their return values to local variables, can annotate function parameters of the relevant type and pass the results of these methods into functions. Their implementation may be magic, but their behavior and semantics all behave exactly like user-defined methods.

As @sjrd pointed out, .checkedCast does not follow any of these rules.

• You cannot assign val y = x.checked and then match on y.

• You cannot define the a method parameter of type def f(y: CheckedCast[Foo]) = y match ... and be forced to pass in x.checkedCast, and have matches in the method body be unchecked

• You cannot define an alias or forwarder def foo[T](x: T) = x.checkedCast and call it instead

In general, you cannot do any of the things you expect with a normal value of a specific type with the result of x.checkedCast.

On one hand, isInstanceOf, eq, Array#apply, etc. behave like methods, so making them look like methods is a unification that reduces confusion. On the other hand, .checkedCast most certainly does not behave like a method, and so making it look like a method would only add confusion.

It’s fine to have things that do not behave like methods. Scala has tons of syntax that do not behave like a method call. But we should make it look like some else - like an annotation, like a keyword, or something else - so that we make it clear that checkedCast is not a method and all the rules/behavior/invariants a user may expect when using normal methods does not apply to checkedCast

[bishabosha]

given that we already have inline foo match ... it would be perhaps less surprising to introduce a new keyword based match open foo match ... or something like that - of course then you need a second syntax for val y :: ys = xs

[odersky]

Exactlty. That’s precisely this splitting hairs which is natural if you design by community or committee, but which leads to a complicated mess in the long run.

[odersky]

On the other hand, .checkedCast most certainly does not behave like a method, and so making it look like a method would only add confusion.

Why does it not behave like a method? It’s what people wished asInstanceOf would be: A cast to what is needed but fully checked at runtime and the compiler will refuse if it can’t be done. The fact that we cannot express this using the standard rules the type system is a technicality from the user’s standpoint. Users don’t understand these rules in their entirety anyway. And we invent new rules all the time and people are cool with that.

I really believe this is another case of splitting hairs, where we draw distinctions that should not matter from the user’s point of view.

[lihaoyi]

@odersky

Why does it not behave like a method?

I gave three concrete examples of things you can do with methods you cannot do with .checkedCast. @sjrd gave a few as well.

You said we create new rules all the time, but I can’t think of any builtin “magic methods” that break these rules. There are some in the community using macros (SBT .value, Mill Task#apply, async/await, sourcecode.*) but none in core language or library. Maybe there’s some Scala3 metaprogramming magic that I’m not aware of

“Nobody cares about rules so we can do whatever” is how you get Lisps. That’s a valid design philosophy: everything is a method call with uniform syntax, regardless of what it means! But it’s not Scala’s philosophy. Scala’s philosophy is that these things do have rules, things like “annotations should not affect typechecking”, “Types can be aliased”, or “expressions can be refactored into named vals according to their evaluation order without change in behavior”.

It’s certainly possible to break these rules - I listed two of my own projects that break them - but it’s not something done lightly, and this case the marginal improvements in an edge case IMO do not justify the breakage

[odersky]

@lihaoyi

As @sjrd pointed out, .checkedCast does not follow any of these rules.

• You cannot assign val y = x.checked and then match on y.

And you cannot write val y = (x: Any).asInstanceOf; val z: Int = y either. It’s target typing at work here, for checkedCast as well as for asInstanceOf. Target typing has limited scope.

@lihaoyi

• You cannot define the a method parameter of type def f(y: CheckedCast[Foo]) = y match ... and be forced to pass in x.checkedCast, and have matches in the method body be unchecked

Don’t understand. Nobody postulated CheckedCast.

@lihaoyi

• You cannot define an alias or forwarder def foo[T](x: T) = x.checkedCast and call it instead

Same holds for asInstanceOf, which proves my point, that checkedCast is just what people wished asInstanceOf would be.

@lihaoyi

“Nobody cares about rules so we can do whatever” is how you get Lisps. That’s a valid design philosophy: everything is a method call with uniform syntax, regardless of what it means! But it’s not Scala’s philosophy. Scala’s philosophy is that these things do have rules, things like “annotations should not affect typechecking”, “Types can be aliased”, or “expressions can be refactored into named vals according to their evaluation order without change in behavior”.

And it was me who created all these rules in the first place. So when I say users would not care about a particular hair split, the strong hypothesis is I know what I am talking about .

@lihaoyi

It’s certainly possible to break these rules - I listed two of my own projects that break them - but it’s not something done lightly, and this case the marginal improvements in an edge case IMO do not justify the breakage

It’s not done lightly at all. It’s what I believe is a breakthrough solution for a long standing malaise, the tension between tighter pattern checking and a simple user-friendly syntax to accommodate that.

[nafg]

@odersky

@nafg

Besides it violates locality – I’d call it spooky action at a distance. Scala is elegant because it avoids that sort of thing, like static members in other languages.

Exactly the opposite is true. We are very precise where we need the checked cast here. By contrast, a language import or compiler setting is spooky action at a distance.

I don’t think language imports are the best solution. But it’s not action at a distance, because all imports, especially language imports, affect the current scope going forward. That is how scopes work.

On the other hand changing the meaning of a pattern, because somewhere else on the line there happens to be syntax that looks like a method but doesn’t return a different value or a different type? That’s just going to get people.

[nafg]

@odersky

Same holds for asInstanceOf, which proves my point, that checkedCast is just what people wished asInstanceOf would be.

Ok I must really be missing something. How is checkedCast at all like asInstanceOf? Does it even take a type parameter?
I guess it’s less checked than an ordinary type ascription upcast? IIRC shapeless had something like that I think?

[nafg]

I reread the beginning of the thread.

To be clear something like

@odersky

  def checkedCast: this.type = this

Is quite method-like and anyone can indeed define that method. That’s not the issue.

The issue is that how pattern matching compiles depends on whether how the scrutinee is written.

For example,

x.checkedCast match ...

would be different than

val y = x.checkedCast
...
y match ...

[odersky]

Ok I must really be missing something. How is checkedCast at all like asInstanceOf ? Does it even take a type parameter?

The type parameter is a technicality as well. In the case of asInstanceOf it can also be inferred (only that is a lot more dangerous than for checkedCast since if for some reason the target type is underdefined, it will insert a cast to Nothing$ instead of complaining at compile-time.)

@nafg

The issue is that how pattern matching compiles depends on whether how the scrutinee is written.

For example,

x.checkedCast match ...

would be different than

val y = x.checkedCast
...
y match ...

I just answered that an hour ago. It’s the same for all target typed things in Scala, whether that’s inferred asInstanceOf, or implicit conversions. Unlike these checkedCast is explicit and bullet-proof.

[nafg]

I’m quoting myself because I wrote this earlier and it didn’t seem like anyone noticed.

@nafg

IIUC the only reason for proposing method syntax is because the previously proposed syntax is not so ergonomic, and this would be more ergonomic.

I think a lot of things would be designed better if the process was framed in a clear problem-solution manner. That is, let’s define clearly what problem(s) we’re trying to solve, and use that as our guide to explore the solution space.

Here’s my attempt:

Problem: Currently patterns can often lead to unexpected runtime errors. Scala is helped popularize the value of preventing runtime errors statically, and as other mainstream languages have now pushed the envelope even further, and developers expect it in more and more places, it’s fitting to change this behavior and prevent such pattern match runtime errors statically as well. However, the current behavior is often desirable, so the language should allow the user to choose whether to pattern match in a safer or less safe way. The syntax for either mode of pattern testing should be ergonomic and intuitive. This is needed for both match expressions, as well as val (or destructuring) patterns. (TBD is this needed for case statement sequences other than match expressions, for anonymous function and partial function literals?)

Is that an accurate and complete description of the problem from scratch? And if yes can we sort of restart the discussion without all the assumptions that were made previously?

[nafg]

I’m really missing something. What does checkedCast do explicitly? What does it cast to?

Type inference, which is indeed affected by the target type, has nothing to do with the problem. asInstanceOf makes sense to be a method because it takes in a value of one type and returns a value of another type. It’s a self-contained bit of “functionality” (even if it were always a no-op at runtime).

Yes target typing can allow the type parameter we are passing it to be inferred. That doesn’t change the fact that once the type parameter is expanded, which is a thing that happens, and it’s not “at a distance” because it’s an obvious part of compiling an expression, the resulting x.asInstanceOf[T] is a self-contained expression, and in its expanded form it can be factored out and moving the code moves the meaning with it.

But AFAICT this method only exists as a way of signaling to a different part of the expression how it should behave, in a way that is not obvious at all.

I don’t know what explicit and bullet-proof means in this context.

Please let’s start from scratch with nothing but a clear problem statement and an open mind.

[odersky]

@nafg

Type inference, which is indeed affected by the target type, has nothing to do with the problem. asInstanceOf makes sense to be a method because it takes in a value of one type and returns a value of another type. It’s a self-contained bit of “functionality” (even if it were always a no-op at runtime).

But all the user cares about asInstanceOf is: I have a static type error, but I know by my own reasoning that the runtime value of an expression fits the expected type. So I insert an asInstanceOf to tell the compiler. checkedCast is like that, only without the pitfalls. It can be perfectly well specified in a formal type system and it would not be difficult to do so.

[nafg]

But what do casts have to do with exhaustivity?