Allow sealed interfaces without subclasses

[Jakob Brünker]

> > Is there a good reason to disallow this? It does come in handy every
once
> > in a while in languages where it's possible, especially when trying to
> > convince the type checker that a particular combination of patterns is
> > impossible.

> Can you share some examples of such situations?

Sure, here's a couple examples of how such a type, and pattern matching on
it, could be used in Java.
Apologies for how long this mail turned out to be, I thought the examples
might not be super helpful
without a bit of context.

---------------------------------------------------------

Example 1:

An empty type can be used to restrict which subclasses of a sum type a
certain value can be an instance of.

Let's say we have some functionality to connect to a server, and this can
result in runtime
errors in production, but no such errors can happen with the mock
connection used in testing.

---------------------------------------------------------

// A error that can occur when connecting
interface ConnError {
  String getMessage();
}

// The type of error you might see in production
record ProdError(String message) implements ConnError {
  public String getMessage() { return message; }
}

// An impossible error, i.e. no values of this type exist (except for null).
// Used during testing.
sealed interface ImpossibleError extends ConnError permits {}

// We use a sum type to encode the fact that setting up a connection either
// succeeds or fail
sealed interface Connection<E extends ConnError>
    permits Connection.Established, Connection.Failure {
  // in actual code, `Established` might carry information about the
connection
  final record Established<E extends ConnError>() implements Connection<E>
{}
  // Failure carries information about the error
  final record Failure<E extends ConnError>(E error) implements
Connection<E> {}
}

// used to connect to the production server, might fail
static Connection<ProdError> connectToProd() {
  return Math.random() > 0.5 ?
    new Connection.Established<>() :
    new Connection.Failure<>(new ProdError("Random failure"));
}

// connecting to the mock server can never fail, the type ensures this
static Connection<ImpossibleError> connectToMock() {
  return new Connection.Established<>();
}

static String runProd() {
  // we have to handle both cases here
  // Note that I'm leaving out the default case since JEP 8213076 says
  // "Knowing that the cases of a switch are exhaustive is useful; it means
  // that we need not manually code default arms that should never be
executed
  // under normal situations."
  return switch(connectToProd()) {
    case Connection.Established<ProdError> conn -> "Success!";
    case Connection.Failure<ProdError> fail -> fail.error().getMessage();
  };
}

static String runTest() {
  // we have to match on both cases but don't have to return anything in the
  // Failure case, since we can prove it's impossible
  return switch(connectToMock()) {
    case Connection.Established<ImpossibleError> conn -> runTestsWith(conn);
    // exhaustiveness checker can see that ImpossibleError has no possible
cases
    // As above, I'm leaving out the default case due to JEP 8213076
    case Connection.Failure<ImpossibleError> fail -> switch(fail.error())
{};
  };
}

---------------------------------------------------------

So by using the empty type as a type argument for a sum type, we can focus
on the
cases that are actually possible when using a value of that type, and have
the
type/exhaustiveness checker make sure that we're not missing anything.

Example 2:

Java has the `void` type to indicate that a method doesn't return a value.
However,
it doesn't say anything about whether the methods returns, in general -
that is, it
can still contain a `return;` statement, without a value. When it's known
that a
method will not return - say, it is guaranteed to always enter an infinite
loop or
throw an exception - it can be useful to encode this on the type level.

In this example, we have a Server that is supposed to run forever, but
might instead
return ValidationErrors while being set up.

---------------------------------------------------------

// Methods with `NoReturn` as return type cannot return (except if they
return null)
sealed interface NoReturn permits {}

// Generic sum type containing a value of one of two possible types;
// We can map over the right side
sealed interface Either<A, B> permits Either.Left, Either.Right {
  <C> Either<A, C> map(Function<B, C> f);

  final record Left<A, B>(A val) implements Either<A, B> {
    public <C> Either<A, C> map(Function<B, C> f) {
      return new Left<>(val);
    }
  }
  final record Right<A, B>(B val) implements Either<A, B> {
    public <C> Either<A, C> map(Function<B, C> f) {
      return new Right<>(f.apply(val));
    }
  }
}

interface ValidationError {}

// imagine this contains something useful
record Config() {}

// returns either all the errors encountered while reading the config file,
// or a valid Config object ready to use.
static Either<List<ValidationError>, Config> readConfig(String configPath) {
  // imagine this parses and checks the config file for errors
  return new Either.Right<>(new Config());
}

// can never return
static NoReturn runServer(Config config) {
  while (true) {
    System.out.println("Doing server stuff...");
  }
  // The compiler is happy with not having a return statement here, due to
the
  // infinite loop
}

// Return type is Either<List<ValidationError>, NoReturn> to indicate that
if
// this function returns,  it will return errors, but it might not return
at all.
// This type is isomorphic to List<ValidationError>.
static Either<List<ValidationError>, NoReturn> setupAndRunServer(String
configPath) {
  return readConfig(configPath).map(Application::runServer);
}

public static void main(String[] args) {
  String configPath = args[0];
  handleErrors(switch (setupAndRunServer(configPath)) {
    Either.Left(var errs) -> errs;
    // We can convince the type checker that we don't need to provide any
    // value here if the function doesn't return
    Either.Right(var noReturn) -> switch (noReturn) {};
  );
}

---------------------------------------------------------

Finally, let me point out that the particular use case I mentioned in my
previous mail, i.e.
> especially when trying to convince the type checker that a particular
*combination* of patterns
> is impossible"
(emphasis added), may admittedly not have been the best example for this
case, since it usually occurs
when dealing with *generalized* algebraic data types, which aren't
supported in Java. (You can emulate
GADTs, and in fact doing that a few days ago that is part of what made me
want to have support for this
kind of empty type, but it's fairly tedious.)

If support for GADTs were improved in some future release, though, this
kind of empty type
could certainly be helpful for using them. (This needn't be direct support
of
GADTs - being able to use lambdas to define generic methods, or support for
higher-kinded type variables, would already make their emulation more
ergonomic.)

On Fri, Nov 27, 2020 at 11:36 PM Brian Goetz <brian.goetz at oracle.com> wrote:

>
>
> >> A final class with a private constructor is what you are looking for.
> >> Like we have java.lang.Void
> > True; My fear is this: Brian Goetz's writeup on pattern matching (
> > https://cr.openjdk.java.net/~briangoetz/amber/pattern-match.html) talks
> > about and https://openjdk.java.net/jeps/8213076 touches on
> exhaustiveness
> > checking. I'm afraid that an exhaustiveness checker won't know that all
> > constructors are private or, if it does, won't know that the private
> > constructors are never called inside the class.
>
> Your fear is well-founded; it is virtually certain the exhaustiveness
> checker would not identify this case.
>
> > Is there a good reason to disallow this? It does come in handy every once
> > in a while in languages where it's possible, especially when trying to
> > convince the type checker that a particular combination of patterns is
> > impossible.
>
> Can you share some examples of such situations?
>