What we have lost ?

[John Rose]

P.S.  There’s a little more to say about empties:
> Taking this all into account, a type `Map<int,Nothing>` is *not* a set 
> of ints.  It is a set that *you cannot take any ints out of*.  It is 
> an empty type, isomorphic to `Nothing` itself (assuming `Nothing` is 
> empty not a unit).

Oops, actually, while it is true that you can’t retrieve any bindings 
from `Map<int,Nothing>`, it is *not* true that the composite type is an 
empty.  It is, in fact, an always-empty set/map.  And *that* is either 
an empty identity object (lots of those to go around, whee!) or else the 
unique empty map of a particular value class.  That latter guy acts like 
a unit type.

I tripped myself up here on a corner-of-a-corner-case named “0^0”. A 
zero-ary replicated product of an empty type is (if I’m keeping score 
right) a unit, not an empty.  (A map is an unordered replicated product 
of tuples, so an empty map is a zero-ary product.  Modulo identity, 
there is only ever just one empty map.)  A unary, binary, or greater 
replicated product of empties is empty, but not a zero-ary.

Going back to arithmetic, an N-way replicated product of type X looks 
like X^N.  An N-way replicated product of an empty looks like 0^N.  That 
in turn is (equivalent to) an empty, so 0^N = 0 for N>0, but 0^0 = 1.

That’s true in the basically logical setting, I think.  Under other 
possible rules 0^0 is 0 or NaN.  I suppose the Java type system could 
adopt the analogs of those outcomes as well for `Map<int,Nothing>`:  It 
could be declared by fiat to itself be a nothing-type (an empty) or a 
static error (that’s the NaN?).

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.org/pipermail/valhalla-spec-observers/attachments/20220909/6458255e/attachment-0001.htm>