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?).
