patterns as types

Brian Goetz brian.goetz at oracle.com
Sun Jan 10 19:44:06 UTC 2021



> I have a question about the static patterns feature described in the 
> last published document [1]. If we have a code such as if (s 
> instanceof Shape.redCube(__)) { ... }, then can Shape.redCube be 
> looked as a "type"? Probably Shape instances are only classified by 
> some field values, but I feel these patterns as ad-hoc types, which 
> could be part of the type system (if we ignore that that they bind the 
> extracted values to some variables).

It depends what you mean by types.  At their most basic, types are sets 
of values, so yes, you could build a type system in which types were 
described by patterns.  (This is a form of _refinement type_.) But, what 
you are describing is a far cry from how the Java type system currently 
works.

That said, "patterns as types" is only a means to an end to at least 
part of what you're trying to do, so let's focus on that instead.

> If they were real types, then for example we could write code like 
> this variable definition:
>     LocalDate.of(__, JANUARY, 1) firstDayOfSomeYear = ...;

What you are alluding to is some form of _imperative match statement_, 
where you take a pattern and forcibly match it to a target.  This 
doesn't require types; it requires either a *total* pattern, or some 
sort of alternative in the event of non-match. This is exactly what 
https://github.com/openjdk/amber-docs/blob/master/site/design-notes/pattern-matching-for-java.md#pattern-bind-statements 
("pattern bind statement") is getting at.

The current thinking is that the LHS has to be a pattern that is total 
(or, optimistically total) on the static type of the RHS, as in:

     Point(var x, var y) = aPoint;

Without encouraging a syntax bikeshed, there are several options for how 
to expose this:

  - A more traditional statement, like "let P = e".  This allows for 
more flexible handling of non-total patterns through an optional "else" 
clause, but is more limiting;
  - Treating this as a generalization of local variable declaration. 
Note that `Foo f = e`, which is currently a local variable declaration 
statement, could be reinterpreted as a pattern bind! Then we could bring 
in other total patterns (such as deconstruction patterns) too.

So the bottom line here is we can get to what you want, without the 
detour of calling the set of values matched by a pattern a "type".

> This can be probably an overkill, but the same technique can be used 
> to solve part of the nullability problem, if we defined a static 
> pattern Objects.nonNull:
>
>     class Person {
>         private final Objects.nonNull(String) firstName, lastName;
>         ...
>     }

This is a cute idea, but it sort of pushes the problem down the street a 
little bit -- how would we type-check assignments to `firstName`?  
Assignments in Java don't throw; we statically type the RHS, and this 
guarantees that, if the RHS can be evaluated at all, the assignment will 
be type-safe and exception-free.  To do this, we'd have to also match 
against the same pattern at the assignment site, which I think would be 
pretty frustrating in practice.

I suspect you're thinking that "it would just throw if it didn't match", 
but that's a pretty new interpretation of both assignment and pattern 
matching; neither is supposed to throw.

Cheers,
-Brian


More information about the amber-dev mailing list