Language feature to improve checked exceptions

[Holo The Sage Wolf]

I do want to write for the record my reasons to prefer the Effect system
approach in the hope to convince you and others about my view, but I do
acknowledge that this discussion is still far, and the relevance of my
words now may only appear when the work on patterns and string templates
will finalize, so unless there is a good reason I will not continue the
discussion further after this message.

Effect System enables a code style that is easier to follow, it hides the
"unimportant" parts (unimportant to the logic) somewhere in the background
and allows you to write as if there are no effects to your code (I am aware
of the irony here). Of course it does in the end force you to handle the
effects, but you can handle those effects orthogonally to your actual
logic. Unlike the Monadic system which requires you to work in "the monad
world" as described a lot by Haskell developers, you need to carry your
Either wraps everywhere till you handle them.

In addition, I believe that there is another argument for the Effect system
specifically for Java: there is a difference between a language feature and
a datatype, unlike some other languages Java is built heavily over 3rd
party libraries, if we look at the big libraries out there we would find
that a lot of them are using custom Either (and friends) classes, this
cause that composing those libraries is not as simple as we would want it
to be, by making a language feature that handle those cases *well*, there
will be a much larger intersection between the APIs (the "*well"*  in the
previous sentence is important, I want to believe that it is possible to do
that in Java)

Finally I want to link 2 more projects.

Apart from Koka there is also [Effekt](https://effekt-lang.org/), I like
the way Koka handles things better, but Effekt is another language that has
Effects as its core mechanic.

Apart from Effect systems, there is also the idea of Coeffect systems, for
a similar reasons as above, I really like a Coeffect type system and want
to link to [my coeffect system in Java](https://github.com/Holo314/Coeffect)
(I didn't have much time to work on it lately, but currently I am fighting
Java's compiler plugins API to make it a stand alone plugin, as well as in
the process of implementing custom type system in the annotation to enable
stuff similar to what I wrote in my previous mail).

Again, I would love to discuss further when it is more relevant.

On Tue, Mar 7, 2023 at 4:56 PM Brian Goetz <brian.goetz at oracle.com> wrote:

> 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:
>
> @FunctionalInterfacepublic interface EPredicate<T, E extends Throwable> {
>     boolean test(T t) throws E;
> }
> @FunctionalInterfacepublic 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
>
>
>

-- 
Holo The Wise Wolf Of Yoitsu
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/amber-dev/attachments/20230307/4d5f9bf4/attachment-0001.htm>