The Forum for Discussion about The Third Manifesto and Related Matters

Please or Register to create posts and topics.

Which type?

PreviousPage 9 of 9

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


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



PreviousPage 9 of 9