Pre SIP: Replace non-sensical @unchecked annotations

[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.

[bjornregnell]

@bishabosha How do you mean “repurpose asMatchable "? That sounds really interesting!

[bishabosha]

so currently we have

package compiletime

extension [T](x: T)
  transparent inline def asMatchable: x.type & Matchable =
    x.asInstanceOf[x.type & Matchable]

Casts a value to be Matchable . This is needed if the value’s type is an unconstrained type parameter and the value is the scrutinee of a match expression. This is normally disallowed since it violates parametricity and allows to uncover implementation details that were intended to be hidden. The asMatchable escape hatch should be used sparingly. It’s usually better to constrain the scrutinee type to be Matchable in the first place.

so could we change the body to add the new : @checkedCast ascription?

[bjornregnell]

This is intriguing! Simple and beautiful! I cannot currently find any downsides to this, other than that we perhaps overload the usage of asMatchable, but it is for a similar purpose, so why not!? The advantage is that the change is minimal and it is already there. (The doc comment needs to be updated in a good way to explain its dual usage, perhaps with a nice set of examples in the doc.)

What do you think @odersky ?

[odersky]

For my taste it would overload asMatchable too much. asMatchable means turn a type (like Any or an opaque type alias) that is usually not matchable into something that is matchable, which risks revealing the implementation of the type in ways that break encapsulation. The danger of asMatchable is that you can then do something you are not supposed to by the type contract. E.g. mutating
an IArray.

The meaning of checkedCast is quite different. I think I also like runtimeCheck as a name.

[bjornregnell]

OK yeah, conflating two usages might not be that good after all. An indication of this not being an optimal solution is that the docs would be long and elaborate for a “repurposed asMatchable”.

It now seems like a ripe time for a conclusion on this:

• Change the name of the annotation @uncheckable to @checkedCast or similar by means of deprecation
• add def runtimeCheck to Predef as an extension that uses the new annotation
  Is this a big enough change to require a SIP? I guess we are conservative with regards to Predef changes - but I’m unsure about the formal process here… @anatoliykmetyuk )

[bishabosha]

@odersky

which risks revealing the implementation of the type in ways that break encapsulation. The danger of asMatchable is that you can then do something you are not supposed to by the type contract. E.g. mutating
an IArray.

my reasoning is that checkedCast is doing the same, e.g. revealing a List unsafely as a ::, maybe there can be similar abuses of encapsulation

[morgen-peschke]

@odersky

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.

@Ichoran

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.

Aside from Conversion doing exactly this, it’s been suggested at least once. Treating things as type is unreasonably useful

[Sporarum]

For what it’s worth: I’m in favor of runtimeCheck as a name, I think it’s the best proposed so far

[robstoll]

I am in favour of runtimeChecked as it aligns better with unchecked IMO

[som-snytt]

if you can take as long as you want, it is untimeChecked

[anatoliykmetyuk]

We discussed with the Scala Center and LAMP team about whether Predef changes warrant a SIP. It’s a tricky question since on one hand we don’t want the standard library to receive special treatment, on the other hand, it already does

So I’d say to be on the safer side it’d be good to pipe the change through the formal SIP process as it does affect the users almost on the level of a change to the language itself.

[odersky]

OK. I won’t have the time to draw up a SIP on this by myself. Is anybody up to co-proposing it?

Just to be clear what we want:

• An extension method in Predef named runtimeCheck.
• Expanding into a new annotation annotation.RuntimeCheck

  extension [T](x: T)
    transparent inline def runtimeCheck: x.type = x: @annotation.RuntimeCheck

[bishabosha]

@odersky

Is anybody up to co-proposing it?

I can do it

[MateuszKowalewski]

Voice from the peanut gallery:

I would prefer the annotation to be called compiletime.assumeType. (Or something along that.)

I think this would give a good experience understanding this feature in case you find some code using it. Code-surfing from runtimeCheck would take you to

extension [T](x: T)
   transparent inline def runtimeCheck: x.type = x: @compiletime.assumeType

This clearly explains the feature in one line, imho.

It’s better than saying two times “runtime check” without noting this involves lessening compile-time safety.

Oh! But what about regular unsafe stuff on Scala Native (which is still “regular Scala”)? Could I call runtimeCheck on some unsafe construct? What would happen? Or would this somehow magically force runtime checks on Scala Native unsafe constructs? (I guess this can’t work like that. But maybe this feature could be disabled for Scala Native unsafe things. If not, it needs some other name, I guess). Or is Scala Native unsafe stuff actually irrelevant here?

---

@odersky

There’s another reason, which is partly how I came to this. We are looking into pluggable refinement type systems. […] The idea would be that we run plugins or custom-phases after the type checker to verify that an Int value is really a Pos, or that a list is non-empty. For instance by running some kind of solver.

This sounds so [[censored]] exciting, I can’t hold my horses!!!

Could this mean that something like Turnstile+ (paper2017, paper2020, code) will come to Scala eventually?

Pluggable, user definable type systems look like the future of programming to me. Very cool Scala could be once more on the forefront of such revolutionary movement!

[odersky]

Great to see you are excited! The project is worked on by @mbovel and some master students at EPFL. For now, it’s strictly research.

[Sporarum]

I don’t know where the project is at right now, but I worked on syntax and runtime checks for it as my Master thesis. You can find my presentation slides here: go.epfl.ch/QT-slides.

But this was very early work, so don’t take anything from there as an indication of what is-to-be.

Notably I was in favor of heavily incorporating qualified types into the language (which you can see reflected in my work), but this has many downsides (and upsides of course), and so might not be chosen as the direction for the project.
(Or might have already been discarded)

Regardless, let’s put the subject aside for now, and I’m sure LARA and LAMP (the two labs working on it) will let us know here when it is more concrete !

[bishabosha]

@bishabosha

I can do it

I didn’t forget if anyone is thinking

Edit: it is posted: SIP-57 - Replace non-sensical @unchecked annotations by bishabosha · Pull Request #67 · scala/improvement-proposals · GitHub

[benhutchison]

Nice work @Sporarum I reviewed your presentation on Qualified Types and am excited about the potential here. I hope this work sees the light of day eventually - I can see myself using this. Perhaps a Qualified Types proposal deserves a dedicated thread at the appropriate point in its development?

One question I was left with was about what scope/context the qualifier expression is interpreted in?

Your examples tended to use standard library built-ins, egs type Pos = Int with _ > 0 and type NonEmptyString = String with s => !s.isEmpty, but > and isEmpty are, more generally, method invocations. What if the qualifier expression invokes a user-defined method, or relies upon an implicit like an Ordering, that need to be brought into scope via an import?

It would be good to see some desugared examples showing how this is intended to operate…

[Sporarum]

Thank you for your enthusiasm !

Here’s the trick: there’s no solver, therefore we don’t need desugarring yet !
It’s all either booleans at runtime or fixed trees at compiletime.

But of course this is not really usable as-is:

val x: Int with x > 0 = 4
val y: Int with 0 < y = x // error: type mismatch

This simple example could be solved with some regularization, but slightly more complicated examples really need a solver to be practical:

val x: Int with x > 10 = 11
val y: Int with y > 0 = x // should succeed ! (but doesn't without a solver)

The internal representation will depend heavily on the solver’s capabilities, so we’ll have to wait and see !

(I’ll maybe open a new thread to discuss all those things, for now let’s leave it at that)