2 ms·

Would you mind expanding on what you mean by "as static types"? As I see it, it's definitely a part of Java's type system that things which throw a checked exc

Would you mind expanding on what you mean by "as static types"? As I see it, it's definitely a part of Java's type system that things which throw a checked exception will require that you handle those checked exceptions. But now here comes `sneakyThrows` and the next thing you know your `Function#apply` (`R apply(I)`, not a `throws` to be seen in that declaration) is throwing a checked exception (not an `UndeclaredThrowableException` wrapping the checked exception, literally the checked exception ... unchecked). But I'll admit I'm rather an amateur when it comes to such things.

munificent 2y ago
To violate soundness, you'd need to get into a situation where an unexpected checked exception leads an expression or variable to end up with a value of some type that doesn't match the expression or variable's static type. This would be easy if the hole worked in the other direction where an exception should be thrown but isn't. Because then you could probably do something like confuse the definite assignment analysis in a constructor body to make it think all fields are initialized by the end of the constructor, like: class C { final int x; C(bool b) { if (b) { thingThatMustThrow(); } else { x = 1; } } } Here, if the control flow analysis expected that `thingThatMustThrow()` will always throw an exception, then it might conclude that all paths that reach the end of the constructor body will definitely initialize `x`. But if that method doesn't throw an exception, then execution could proceed merrily along and `x` never get initialized. (In practice, this isn't an issue because field definite initialization analysis is already unsound so the VM default initializes every field anyway.) But in this case, it goes in the other direction. You have code that isn't expected to throw that does. I can't think of a situation where that would lead Java to end up with a value of the wrong type flowing somewhere unexpected.
- svieira 2y ago
  Ah, "static" in the sense of "statically analyzable" because it's part of the typing phase. And "sound" here meaning only that the program can only assign values that match the statically determined types. Interesting that "soundness" doesn't include typing effects (at least in the literature), but I guess general typed effects are relatively new and we aren't yet at the point where Koka-like effect types are "expected functionality" when building a new programming language. Thank you so much!

munificent 2y ago

To violate soundness, you'd need to get into a situation where an unexpected checked exception leads an expression or variable to end up with a value of some type that doesn't match the expression or variable's static type. This would be easy if the hole worked in the other direction where an exception should be thrown but isn't. Because then you could probably do something like confuse the definite assignment analysis in a constructor body to make it think all fields are initialized by the end of the constructor, like: class C { final int x; C(bool b) { if (b) { thingThatMustThrow(); } else { x = 1; } } } Here, if the control flow analysis expected that `thingThatMustThrow()` will always throw an exception, then it might conclude that all paths that reach the end of the constructor body will definitely initialize `x`. But if that method doesn't throw an exception, then execution could proceed merrily along and `x` never get initialized. (In practice, this isn't an issue because field definite initialization analysis is already unsound so the VM default initializes every field anyway.) But in this case, it goes in the other direction. You have code that isn't expected to throw that does. I can't think of a situation where that would lead Java to end up with a value of the wrong type flowing somewhere unexpected.

svieira 2y ago
Ah, "static" in the sense of "statically analyzable" because it's part of the typing phase. And "sound" here meaning only that the program can only assign values that match the statically determined types. Interesting that "soundness" doesn't include typing effects (at least in the literature), but I guess general typed effects are relatively new and we aren't yet at the point where Koka-like effect types are "expected functionality" when building a new programming language. Thank you so much!