Language feature to improve checked exceptions

[Brian Goetz]

Thanks for the link to Koka.

Indeed, I spent many hours prototyping something exactly like this for 
Streams back in the Java 8 days, as an extension to one of the 
"exception transparency" proposals that came up at the time.  As you 
point out, in libraries like streams, a throwing lambda passed as a 
parameter "pollutes" the type of the returned stream, since the lambda 
is incorporated into the stream and may be invoked by a later operation, 
and therefore might be thrown from that later operation.

This basically asks the generic type system to have type variables to 
track effects as well as types (see, e.g., "Type and Effect Systems", 
Nielsen and Nielsen.)

As your example shows, it is possible to do this with (a) some form of 
variadic generics and (b) some algebraic operations on variadic 
parameters (e.g., concatenating, unioning, differencing).  It also means 
that generic classes like Stream have to carry around additional type 
variables describing their exceptions (effects), and those tvars are 
"different" from ordinary tvars.

Our conclusion at the time we did this experiment is that, while the 
approach is viable, annotation burden on library authors is high, and 
this burden flows through to clients as well.  (Even if we allow use 
sites to elide the exception information, so they can say Stream<String> 
rather than Stream<String, ExceptionGoop>, it still flows into the docs 
and error messages.)  It also makes generics "even more complex" (and 
people still complain generics are too complex.)

So the outcome of this experiment was "yes, it can be made to work, but 
no, we don't think putting into Java at this time is likely to be seen 
entirely positively."

> While I do believe that the actual solution will require much more 
> thought than this (e.g. deconstruction of generic sums to be able to 
> handle specific exceptions and remove those exceptions from the final 
> union type of exceptions), this is a showcase that a nice and 
> composable checked exceptions works even without Monadic types.
>

Indeed. The need for asymmetric difference as one of the algebraic 
operations on effect variables is one of those surprises that bites you 
the first time you encounter it.

> I find this direction much nicer than using Either everywhere.
>

I am not sure whether I do or not, which is one reason we've not done 
either yet...



On 3/7/2023 8:24 AM, Holo The Sage Wolf wrote:
>
> This is a continuation of this thread 
> <https://mail.openjdk.org/pipermail/amber-dev/2023-March/007849.html>, 
> unfortunately I only joined the mailing list, so I can’t reply to it 
> so I apologize for opening a new thread.
>
> I want to point to Koka 
> <https://koka-lang.github.io/koka/doc/book.html#why-effects>, Koka is 
> a language built upon the concept of Effect, a generalization of how 
> Java treats checked exceptions (and similarly to what Brian Goetz said 
> about how Checked exceptions are equivalent to Either, general Effect 
> system is equivalent to full monadic type system).
>
> The language is very interesting and worth reading about, but the 
> relevant part is their Polymorphic Effects, which allow you to extend 
> the effects. In Java pseudo code, it means that the following is valid:
>
> |@FunctionalInterface public interface EPredicate<T, E extends 
> Throwable> { boolean test(T t) throws E; } @FunctionalInterface public 
> interface EConsumer<T, E extends Throwable> { boolean test(T t) throws 
> E; } public class EStream<V,E extends Throwable> { public <EX extends 
> Throwable> EStream<V, (E|EX)> filter(EPredicate<? super T, (E|EX)> 
> predicate) { ... } public <EX extends Throwable> void 
> forEach(EConsumer<? super T, (E|EX)> action) throws E, EX { ... } } |
>
> Which allows you to have a fluent composition without losing the 
> fine-grained checked exceptions:
>
> |public static void main(string[] args) throws FileNotFoundException, 
> IllegalAccessException, SQLException { myEStream.filter(v -> ...) // 
> something that throws FileNotFoundException .filter(v -> ...) // 
> something that throws IllegalAccessException .forEach(v -> ...); // 
> something that throws SQLException } |
>
> This also makes the type system of the |throws| clause a subset of the 
> generics type system.
>
> While I do believe that the actual solution will require much more 
> thought than this (e.g. deconstruction of generic sums to be able to 
> handle specific exceptions and remove those exceptions from the final 
> union type of exceptions), this is a showcase that a nice and 
> composable checked exceptions works even without Monadic types.
>
> I find this direction much nicer than using Either everywhere.
>
> -- 
> Holo The Wise Wolf Of Yoitsu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20230307/d934f3cb/attachment.htm>