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