Switch expressions spec

[John Rose]

On Mar 15, 2019, at 11:39 AM, Alex Buckley <alex.buckley at oracle.com> wrote:
> 
> In a switch expression, I believe it should be legal for every `case`/`default` arm to complete abruptly _for a reason other than a break with value_.

My reading of Gavin's draft is that he is doing something very
subtle there, which is to retain an existing feature in the language
that an expression always has a defined normal completion.

We also don't have expressions of the form "throw e".  Allowing
a switch expression to complete without a value on *every* arm
raises the same question as "throw e" as an expression.  How do
you type "f(throw e)"?  If you can answer that, then you can also
have switch expressions that refuse to break with any values.

BTW, if an expression has a defined normal completion, it also
has a possible type.  By possible type I mean at least one correct
typing (poly-expressions can have many).  So one obvious
result of Gavin's draft is that you derive possible types from
the arms of the switch expression that break with values.

But the root requirement, I think, is to preserve the possible
normal normal of every expression.

"What about some form of 1/0?"  That's a good question.
What about it?  It completes normally with a type of int.
Dynamically, the normal completion is never taken.
Gavin might call that a "notional normal completion"
(I like that word) provided to uphold the general principle
even where static analysis proves that the Turing machine
fails to return normally.

— John