-
Notifications
You must be signed in to change notification settings - Fork 73
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support cast-free Java arrays #138
Comments
By “casts”, are you referring to the runtime checks that Java needs on array assignment? Do you imagine eliminating the checks by compiling this loop with code duplication, one copy specialised to nums being Integer[]? If so, this doesn’t strike me as a particularly convincing example. If computational performance did matter for some numeric computations, then you probably wouldn’t be using arrays of wrapped number types for it, which are heavy in Java. It’s a fairly safe bet that object allocation would dominate this example, not runtime checks. Also, I don’t understand how your simplification of making that a field (on Having said all that, can you clarify the actual problem you see? Can you explain why you think that the MVP would get in the way of a later extension with some form of existential typing, as you probably have in mind to enable this? |
I am referring to the same casts I referenced in the issue I reference in the OP: #120. "Superfluous" is the term we have been using to specifically refer to casts that do not exist in the source language (or in standard compilations of the source language) but which exist in compilations to the current MVP due to its limitations in reasoning about common invariants.
Please see this presentation you attended a month ago, which is a recap of the discussion you and I had on this topic nearly three years ago, and which discusses this particular example (slide 28). You might also refer to the e-mail 7 months ago where I illustrated why the self types you had planned to propose at the in-person meeting would be unable to express this particular example. Or you can refer to Juan Chen and David Tarditi's POPL '07 paper that first discussed the issues with self types, among other structural approaches, and addressed them with nominal types (e.g. #119). To summarize, concerns are expressiveness, decidability, and practicality of generation. |
So is this essentially the same example as #120, with your point again being that "bounded quantification + structural typing is undecidable"? |
Roughly. #120's example was designed to test run-time design aspects, whereas this example is designed to test compile-time design aspects. Though it occurs to me that a related challenge is being able to allocate an |
Maybe unfortunate to use What if instead we're talking about Agree that at a source level this should not need casts. Would say that doesn't sound like the best example, and be better to have a more realistic example of something a) people commonly write, b) without dynamic allocation inside the loop (i.e. something you'd expect to be fast), and c) with a type of object that you reasonably would expect to be a dynamically allocated object with subtyping. |
@aardappel Somewhat surprisingly, it does not matter if this example itself requires good performance or not. The reason is that, if the Post-MVP cannot express this example, and in particular provably maintain the invariant that a Java I did a quick benchmark for sorting an array of a |
The "closed" update above does not appear to make sense. Rebasing artifact or typo? |
I honestly have no idea. I did not close anything, GitHub just randomly closed some issues, not just this one. Maybe it somehow magically inferred something from the merge commit message? That's why "smart" UIs are such a bad idea... Edit: Yeah, I think what happened is that I merged upstream, which involved some upstream commits saying "Fixes #X" in the upstream repository. Then GH smartly interpreted those in stupid ways. =-O |
Closing this because it is non-actionable for the MVP. I've labeled it post-MVP, though, so it's easy to find again once we start looking to do follow-on work. |
#120 suggests that superfluous casts can cause significant overhead for array-intensive programs. Please illustrate how the Post-MVP will eliminate these casts. For example, give the WebAssembly translation of the following:
The text was updated successfully, but these errors were encountered: