Last time I asked this was 2021, 4 years later this is still experimental and it seems more and more like it’s never going to be included.
I think at this point the feature has been experimental for the longest time (of all features that were in experimental), and it can’t be due to lack of testing or experimenting with, as it hasn’t really gone thru any more development-feedback cycles.
Might be a good time to just cull it.
erased is still a key feature for what we want to achieve. Done correctly it will enable compile-time capabilities without a runtime footprint. There are lots of valid use cases for that. But to get there we need to make sure erased definitions are capability-safe, i.e. that they don’t permit to create capabilities from nothing. We did not yet find the time to work on this, but it’s on the todo list.
I consider erased essential because it is the only way to add strict-equality support to libraries (including the standard library) without breaking binary compatibility.
None of this was my point, you answered on the desirability of the feature based on the use you want to give it.
Erased started its journey back in feb 2018 (if my github browsing is correct), way before capabilities were conceived: What has prevented them in 7 years from becoming non-experimental? At this point either commit to them or remove them, is my point.
There’s always going to be a “the next feature will fix it all, I promise”, but today the feature should either stand on its own or not, and not is clearly the answer this time. Even with erased gone, capabilities can be done simply with details about how the compiler achieves it hidden from the user, so once again erased a keyword isn’t justified (if it weren’t already in all these years).
(In case one wonders “why do you care? it doesn’t take up space”, I do get quite a bit of negative feedback on scala3 for all of its seemingly incomplete or under-delivered features, and I feel like reducing the experimental budget/scope would be quite nice for stability and outside appearance.)
if you read about implicit function types, capabilities was always the intention: Implicit Function Types | The Scala Programming Language (2016)
Oh that, I guess you’re right and I stand corrected, thanks. I was referring more so to the new special type lattice if you will around capabilities.
From this and some other clues, it sounds like you interpreted Martin as saying “We can implement erased with capabilities (so no erased for you until they get there)”
Which I don’t think was the message, but rather: “If we make a mistake implementing erased, it will ruin the whole point of capabilities (so we might as well get it right)”
Here is an example of the kind of problems that arise with erased:
erased def magic: Nothing = magic
val x: Int = magic
Naively, this type checks !
magic (left) has type Nothing because magic (right) has type Nothing
And Nothing is a subtype of Int (because it’s a subtype of everything)
Without erased, there is no problem: magic would loop forever, and thus never return anything
With erased, it disappears from the runtime, so there is no infinite loop preventing us from using x
And you can construct much more devious examples !
To go further:
There is an equivalence between values/types and proofs/statements and there a value of Nothing is equivalent to a contradiction: a proof of every statement (and its opposite)
Which I don’t think was the message, but rather: “If we make a mistake implementing erased, it will ruin the whole point of capabilities (so we might as well get it right)”
That hadn’t occur to me, thanks. I guess in my head erased is its own thing and not as conflated to capture checking so I didn’t think of this. I’m now unsure on whether my perspective is wrong.
Here is an example of the kind of problems that arise with
erased:
I couldn’t follow the example. That code would not type-check, you can’t assign an erased expression to a non erased val, no?
I should have been more clear, I said “naively” to imply this wasn’t what was specced
To understand better why it’s hard to be sure erased is safe let’s take the problem from the other end:
erased is perfectly sound if you completely isolate it from anyhing non-erased
But a system like that would make it useless !
Because your program has at least some runtime behavior, aka non-erased, so you cannot use your erased values at all
Therefore for erased to be useful, there needs to be some interaction between those two worlds.
And it’s really hard to make sure those interactions don’t make a version of magic possible/usable !
Alright, but now we are back at the 7 years have passed already, for the most part with no iterations on the feature too (or maybe I haven’t been paying attention?).
Wouldn’t that be enough maturing time? (again stressing on the no iterations on the feature part, and again assuming I got this right)
The issue is:
erasederased might be fine with today’s capabilities, but not for tomorrow’sI do however understand the frustration with how long some things are taking, especially given the usefulness of erased !
It’s worthwhile to consider that the team working on the typechecker is quite small, and working on other things as well, which make it less surprising things take years
It typechecks, but it shouldn’t pass the erasure check because the value of magic is (nominally) used. This has nothing to do with capabilities, just whether the erasure checker knows whether a value is actually needed. It obviously needs to be done carefully, but there are a variety of cases (e.g. inlining) where one tries to a certain depth and then gives up. But in this case that doesn’t even matter; as soon as you see val x: Int = <erased>, you know it’s wrong. The compiler needs to avoid an infinite loop itself when evaluating erased def magic: Nothing = magic, but that’s it.
If something like this has any chance whatsoever of breaking capabilities at the type level, I submit that capabilities might be on too fragile of a theoretical foundation. If, on the other hand, the type level is fine but the implementation of checking is complicated and might give the wrong answer for particular instances, then I understand, but that doesn’t seem like a blocker for making erased stable. You just declare what it is supposed to do, and if there are implementation bugs then you fix the bugs.
Now, if it is not known whether capabilities might be on a fragile theoretical foundation because it’s all simply too new, then it makes sense. The soundness holes in f-bounded polymorphism used as a mytype are obvious when you know what to look for, but harder to recognize the first time.
But then I think the fairer thing to say is just, “Look, we have this whole system where we carry around permissions and check properties that are just a compiler fiction, and erasure is a really powerful fiction, and it’s complicated to know whether it will let us pretend the wrong things.”
Here’s a capability example:
import java.io.IOException
class CanThrow[-E <: Exception]
def foo[E <: Exception](e: E)(using erased CanThrow[E]): Nothing = throw e
erased def magic[E]: E = magic
def Test = foo(new IOException)(using magic)
Here, magic is only used to be passed to the erased parameter of foo. So no use of erased stays in the program. But the program is obviously not capability safe, since we made up the CanThrow from nothing.
I believe we need to do two main changes to get capability-safety:
So right off the bat my usages of erased are already invalid 
.
By the way, from what I’m testing in 3.7.1 and from what I’m reading in the docs, nothing prevents non erased terms to be passed to erased positions, so:
import java.io.IOException
class CanThrow[-E <: Exception]
def foo[E <: Exception](e: E)(using erased CanThrow[E]): Nothing = throw e
def magic[E]: E = null.asInstanceOf[E]
def Test = foo(new IOException)(using magic)
Would be valid even under the extra rules. Furthermore null doesn’t allocate, and because an erased value can’t be used in non erased position, nothing could even dereference it to see that it’s null and not a CanThrow.
No, that would violate the second requirement:
magic[IOException] is not an immutable value and null.asInstanceOf[E] is not one either. So, basically the only functions one can use in an erased context are inline functions that disappear before erasure.
Thanks, I had misread that second clause, I see it now. I’m on the edge about it since it would basically shift the way you write code, from regular functions with using (to derive logic) to inline functions using compiletime. Seems annoyingly like two different syntax to accomplish the same.
I’m startled by this statement
null.asInstanceOf[E]is not one either
how is a singleton not an immutable value? I don’t know any other definition of immutable value that would rule this one out. Interestingly Scala makes casts look like method/functions, and sure one can argue that arbitrary method calls have no guarantee to be constant, but this feels quite wrong to qualify this as not immutable. The equivalent java code would be immutable since there’s no function/method call.
I would disagree as well that asInstanceOf is a form of mutation (since it’s a no-op at runtime), but rather that we should disregard it with regards to type safety, as it’s whole point is to side step the type checker:
4.asInstanceOf[String]
It’s not even guaranteed that a runtime error will be emitted
(Which a lot of people get wrong, since in simple cases you do often get a class cast exception from the JVM)
Immutability is besides the point. null.asInstanceOf[E] is not a value.
But we can make up all kinds of things from nothing. For instance, we can
def magic[E]: E = null.asInstanceOf[E]
Seq(Array(1, 2, 3)).sorted(using magic)
and it compiles.
But wait! null is an Ordering!
Seq(Array(1, 2, 3)).sorted(using null)
works too! It’s just a problem with universal-ish subtypes that promise what they can’t deliver.
The Ordering isn’t erased; it just happens not to be needed to “sort” a list of length 1. So it works, even though it wouldn’t compile without using magic (or a null).
Maybe the point is that with capabilities, even though we’ve always been able to do this, the guards on “promising something” need to be tighter than they’ve ever needed to be in the past because we anticipate many more promises where the promise does not itself implement anything.
I think inline defs would be okay, though?
Can you explain a bit what your usages are?