>But what is the range of the expression (len - 1)?
Ill-defined, which is as it should be. Naturals are not closed under subtraction or negation, and therefore you should never negate or subtract a length.
You subtract lengths from other lengths all the time. How far have you gone recently? How much taller are you than your wife? Subtracting a length from another length isn't a problem at all; a problem would be if you wanted to subtract a length from a weight.
This
> Naturals are not closed under subtraction or negation, and therefore you should never negate or subtract a length.
assumes that a paramount goal in having types is to make function signatures like the following impossible:
public static String format(String format, Object... args);
Infinite-dimensional vectors (in which the first element is a String) sure aren't closed under format -- it maps them to scalars! But somehow string formatting is wildly popular. Or think of
public Color(int r, int g, int b);
public Color(int rgb);
Are you comfortable having a mapping from ℤ to Color, and from ℤ^3 to Color? If so, why does it bother you less than a mapping from ℤ ∩ [0, ∞) to ℤ ∩ [-1, ∞)?
Try a simple rewording of your argument: Hash tables aren't closed under access. Therefore, you should never retrieve values from a hash table.
>You subtract lengths from other lengths all the time.
Indeed. Notice that all your examples are physical lengths. This is of a different type than the naturals (digital lengths). We generally consider physical lengths to be in the domain of Reals, usually defined along a particular path or dimension. This is closed under subtraction, while naturals are not.
> a problem would be if you wanted to subtract a length from a weight.
That is also a problem, not the only problem.
>assumes that a paramount goal in having types is to make function signatures like the following impossible: [vomit-inducing variadic signature]
I would sure like it if function signatures like that were impossible :)
> Infinite-dimensional vectors (in which the first element is a String) sure aren't closed under format
It's very generous to call a set of arguments to variadic function a "vector" at all, and they certainly aren't infinite-dimensional. They are practically bounded by machine memory.
>it maps them to scalars
How?
>But somehow string formatting is wildly popular.
Lots of mathematically ill-defined things are wildly popular.
> We generally consider physical lengths to be in the domain of Reals, usually defined along a particular path or dimension. This is closed under subtraction
This is wrong. We consider physical lengths to be nonnegative real numbers, which are not closed under subtraction. Trying to use negative numbers for physical lengths will get you very funny looks.
> It's very generous to call a set of arguments to variadic function a "vector" at all
It's not an element of a mathematical vector space, but it's a vector in the common sense of an ordered collection of values. The other examples I gave you, like (int, int, int), are vectors even in the algebraic sense.
> I would sure like it if function signatures like that were impossible :)
That was the signature for Java's String.format, the equivalent of C's sprintf (which, like String.format, maps an infinite-dimensional vector to a single string). If you really didn't understand this, you can tell that the return type from String.format is a scalar by looking at the return type declaration, "String". To understand the precise mapping, I can only recommend you read the javadoc.
>> But somehow string formatting is wildly popular.
> Lots of mathematically ill-defined things are wildly popular.
I'm willing to grant this, but it's certainly not relevant to string formatting.
>> Hash tables aren't closed under access.
> Not sure what you mean by this.
Accessing a hash table isn't guaranteed to get you another hash table. Just like subtracting two positive numbers won't necessarily get you a positive number.
Subtracting two length doesn't give you a length, it gives you a difference of length, which can be any real number.
So by analogy subtracting two unsigned ints should give you a signed int by default (unless you specifically ask for the unsafe unsigned int, and then it's on you to make sure the preconditions are met).
Ill-defined, which is as it should be. Naturals are not closed under subtraction or negation, and therefore you should never negate or subtract a length.