Which type?
So we ended up arguing about whether "values have type" in the other topic I started about if "function/operator(s) can return only one result".
I thought of an example that might (but I rather suspect not) help on this topic, and I thought it should go in the original topic.
It is not known ifย ๐๐ is irrational.
We know that (regardless of how we represent it) ๐๐ is a real number. We know, in short, that it is "a thing".
Therefore I cannotย - unless I have some newly found mathematical proof (and hopefully some nice big mathematical prize)) to hand - correctly say
๐๐:irrational
Now, I'm sure someone will say that ๐๐ is ofย (or at if you prefer) (most specific) typeย real and hence does not contradict the "all (scalar) values carry with them (at least one) type" claim.
If we discover that ๐๐ is (or is not) irrational, does that change what the value ๐๐ is? Is it's type (conceptually or otherwise) part of its value?
BTW, I'm not asking just to be a pain, I (think) I genuinely don't fully understand the "carry with them" concept of the statement "values shall always carry with them, at least conceptually, some identification of the type to which they belong".
I understand the "value at type" idea - a value being the current value of a variable (or inout/output from an operator, or indeed, the value of an attribute in a relational tuple) that is constrained to be a given (named) set of values. The given name being the value in the phrase "value at type".ย I just don't get what it (or "carry with") means when a value appears as-is/standalone. Where is the information held of what the type of a value is?ย A "catalog" relation? But then, that is just a set, and if a type is more than just a set, what information makesย it more than just a set? If that information is "well that set is used in constraints and is the set of input/output values for some operators", fine. But that is quite a wooly definition for something (that should be, if it is in your foundation) claimed to be axiom concept.
If I create a new value, which I uniquely represent by *Y! but I fail to give it a type, then someone would say, well, it is of type notBool at the very least - hence it does not contradict the "all values carry with them (at least one) type" claim.
If I then say, oh, I've just discovered that *Y! is a real, and I add it to the set of (representable) reals, so it's (most specific) type is now real, would you say that is not the same value that I started with?
If I say, oh, I've just discover that George Boole was wrong, and there are actually three true values, and *Y! is the third truth value...ย well, permission to shoot me frankly. :-)