# Which type?

Quote from Paul Vernon on November 18, 2021, 11:40 amSo 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

`๐๐`

isofย (oratif 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'stype(conceptually or otherwise)partof its value?BTW, I'm not asking

justto 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

justa set, and if atypeis 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. :-)

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