Relaxed assignment conversions for sealed types

Brian Goetz brian.goetz at
Tue Nov 24 15:35:20 UTC 2020

> I agree Brian's really onto something with suggesting the totality 
> question is the same for the two features.  I'm in favour of going 
> even further and removing the cast to allow = to do double duty here 
> for sealed types rather than introducing new syntax for it.  The new 
> syntax ("__ construct" or "(total BarImpl)") highlights "this is 
> different" and I'm not sure we need to do that for sealed types.  
> Letting ='s do the work feels like a better form of auto-boxing where 
> javac does the compile-time analysis and errors out for non-total 
> cases or inserts the required total cast for the user.  This gives 
> both compile time checking and runtime safety without needing to beat 
> the reader over the head about it.
> We want to make it easier to read & write correct code - pushing the 
> analysis of totality for sealed types into javac does both for us.

To connect to the mail that crossed with Dan's, Dan is voting for:

  - Allowing `P = e` when P is optimistically total on the static type 
of `e`

In reviewing the discussions on this over the past few years, what I'm 
seeing is that this requires a certain degree of "getting comfortable" 
with it.  At first, locutions like this seemed woefully imprecise, and 
everyone got nervous, but over time, people have been coming around to 
it.  The "bargaining" stage involves things like "stick `let` in front 
of it", "allow it for locals, but not method parameters", and "require 
it to be strictly total (or total only with null remainder.")   Over 
time, many of these proposed restrictions are seen to be "bargaining" 
with change, and we get comfortable with them.

Dan's observation here is that, with a suitable interpretation of total 
pattern match as a generalization of local declaration, we don't need 
the cast at all, so we sidestep the question.

That said, even if we do that, we're not totally out of the woods, for a 
minor and major reason.

The minor reason is the use in expressions.  Suppose we have a context 
where we are limited to expressions, not statements (e.g., field 
initializers, constructor arguments, etc.) or where we just don't want 
to use a statement for aesthetic reasons.   We still have to use a cast 
in these cases, and the cast is still blind.  But that's minor.

THe major reason is that we still don't have a way to say "this 
statement switch is total, please typecheck that for me."  I don't see a 
way we get to inferring this, which means we need some syntax.  Being 
able to reuse the same syntax in other contexts (e.g., casts) may 
reinforce it in both places.

More information about the amber-spec-experts mailing list