JEP draft: Sealed Types for the Java Language (Preview)

OwnerBrian Goetz
TypeFeature
ScopeSE
StatusSubmitted
Componentspecification / language
EffortM
DurationM
Reviewed byAlex Buckley
Created2019/07/01 19:45
Updated2019/08/19 20:50
Issue8227043

Summary

Enhance the Java programming language with sealed types. Sealed types are classes or interfaces that impose restrictions on which other classes or interfaces may extend or implement them.

Motivation

Java's type system allows us to answer questions like "Is a Circle a kind of Shape?", but gives considerably less help with questions like "What are the kinds of Shape?" The type system is no help at all when it comes to a library restricting which classes can implement a library's types; this means that even if the design intent of the library's is that a given type only has a specific set of subtypes, this cannot be enforced, and therefore cannot be assumed by the implementation. (Access control allows the library author to constrain which packages can access and therefore implement the library, but cannot distinguish an implementer from a user.)

Being able to capture statements like "A Shape is either a Circle or a Rectangle" in the type system not only provides useful documentation to users, but also allows the Java compiler to perform better type checking, since it can exhaustively enumerate the known subtypes. It also allows library implementations to more reliably reason about the behavior of known implementations, since they can be restricted to the same maintenance domain.

Sealed types serve as a useful source of exhaustiveness information for pattern matching. Sealed types and records taken together form a construct often referred to as algebraic data types.

Goals

Enable classes and interfaces to limit permitted subtypes to an enumerated set of types in the same maintenance domain as the type itself.

Non-Goals

It is not a goal to provide new forms of access control such as "friends", or to provide fine-grained control over member overriding.

Description

A sealed type is one for which subtyping is restricted according to guidance specified with the type's declaration. (Finality can be considered a strong form of sealing, where subtyping is prohibited completely.)

Sealing serves two distinct purposes. The first is that it restricts which classes may be a subclass of a sealed class. The second is that it potentially enables exhaustiveness analysis at the use site, such as when switching over type patterns for an instance of a sealed type.

We specify that a class is sealed by applying the sealed modifier to a class or interface, with an optional permits clause:

sealed interface Node
    permits A, B, C { ... }

With an explicit permits clause, Node may be extended only by the types enumerated by the clause, which further must be members of the same module, or, if in the unnamed module, the same package.

In many situations, this may be overly explicit. If all the subtypes are declared in the same compilation unit, we can omit the permits clause, in which case the compiler infers a permits clause by enumerating the subtypes declared in the same compilation unit.

Anonymous subclasses (and lambdas) of a sealed type are prohibited.

Abstract subtypes of sealed types are implicitly sealed, unless declared with the non-sealed modifier.

Concrete subtypes of sealed types are implicitly final, unless declared with the non-sealed modifier.

Sealing, like finality, is enforced by both the language compiler and by the JVM. The sealed-ness of a type, and its list of permitted subtypes, are reified in the class file and enforced at runtime.

Grammar

NormalClassDeclaration:
  {ClassModifier} class TypeIdentifier [TypeParameters]
  [Superclass] [Superinterfaces] [PermittedSubclasses] ClassBody

ClassModifier:
  (one of)
  Annotation public protected private
  abstract static sealed final non-sealed strictfp

PermittedSubclasses:
  permits ClassTypeList

ClassTypeList:
  ClassType {, ClassType}

Restrictions

Compiled form of a sealed type

The class file of a sealed type must have a PermittedSubtypes attribute, which enumerates the permitted subtypes. If the sealed type's declaration in source code lacks an explicit permits clause, the set of permitted subtypes is computed at compile time to be those subtypes of the sealed type which are declared in the same compilation unit as the sealed type.

PermittedSubtypes_attribute {
    u2 attribute_name_index;
    u4 attribute_length;
    u2 permitted_subtypes_count;
    u2 classes[permitted_subtypes_count];
}

Reflection API

The following public methods have been added to java.lang.Class:

The method getPermittedSubtypes() returns an array containing java.lang.constant.ClassDesc objects representing all the permitted subtypes of this class if it is sealed, and returns an empty array if this class is not sealed.

The method isSealed returns true if the given class or interface is sealed. (Compare with isEnum.)

Alternatives

Some languages have direct support for algebraic data types, such as Haskell's data feature. It would be possible to express ADTs more directly and in a manner familiar to Java developers through a variant of the enum feature, where a sum of products could be defined in a single declaration. However, this would not support all the desired use cases, such as those where sums range over classes in more than one compilation unit, or sums that range over classes that are not products.

The permits feature allows a sealed type, such as the Node interface shown earlier, to be accessible-for-invocation by code in any module, but accessible-for-implementation by code in only the module of the sealed type. This makes the type system more expressive than the access control system. With access control alone, if Node is accessible-for-invocation by code in any module (because its package is exported), then Node is also accessible-for-implementation in any module; and if Node is not accessible-for-implementation in any other module, then Node is also not accessible-for-invocation in any other module.

Dependencies

Sealed types go well with records, which in turn lend themselves naturally to pattern matching. Switches over targets whose types are sealed can additionally be checked for exhaustiveness using sealing information when the patterns in the switch are type patterns or total deconstruction patterns.