<!DOCTYPE html><html><head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body><div style="font-family: sans-serif;"><div class="markdown" style="white-space: normal;">
<p dir="auto">P.S. There’s a little more to say about empties:</p>
</div><div class="plaintext" style="white-space: normal;"><blockquote style="margin: 0 0 5px; padding-left: 5px; border-left: 2px solid #777777; color: #777777;"><p dir="auto">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).</p>
</blockquote></div>
<div class="markdown" style="white-space: normal;">
<p dir="auto">Oops, actually, while it is true that you can’t retrieve any bindings from <code style="margin: 0; padding: 0 0.4em; border-radius: 3px; background-color: #F7F7F7;">Map<int,Nothing></code>, it is <em>not</em> true that the composite type is an empty. It is, in fact, an always-empty set/map. And <em>that</em> 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.</p>
<p dir="auto">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.</p>
<p dir="auto">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.</p>
<p dir="auto">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 <code style="margin: 0; padding: 0 0.4em; border-radius: 3px; background-color: #F7F7F7;">Map<int,Nothing></code>: It could be declared by fiat to itself be a nothing-type (an empty) or a static error (that’s the NaN?).</p>
</div></div></body>
</html>