The Third Manifesto ForumThe Third Manifesto: TTM General discussion'Phantom type' for Attribute-Valu …

Please or Register to create posts and topics.

'Phantom type' for Attribute-Value pairs, in "popular languages" [was C# as a D]

#11 · June 21, 2020, 12:34 pm

Quote from AntC on June 20, 2020, 2:58 am

So a Tutorial D/IM question:

Is it allowed to form a UNION type with only one type element?

Presumably that UNION type's name is distinct from the name of its based-on type(?)

Presumably the type still needs a tag to Select values of the UNION, even though all such values have MST of the based-on type(?)

What is the type of that tag/Selector?

Can I form a UNION type name CITY with Selector CITY that selects a CHAR? (How) is CITY('Delft') (or however you write it) distinguished from plain CHAR 'Delft'?

Allowed, probably yes because the TTM authors are generally reluctant to rule out degenerate cases merely because they're "not useful anyway". Useful, seems like no.

Yes the name must be distinct.

No, no selectors are introduced because in general union types cannot be guaranteed to have possreps that can render every single value of the union. And selectors are tied to possreps.

So, "that tag/selector" generally does not exist.

I'm too puzzled by the fifth question.

Oh yes, and that's of course the IM version of UNION types. If you're talking of trying to get the notional equivalent of union-types-of-the-literature outside the IM but inside TTM, then you're on your own getting a regular scalar type defined (say I want to UNION CHAR and INT) with a possrep along the lines of

POSSREP ... (VALUETYPE STRING, VALUE STRING) CONSTRAINT (VALUETYPE = 'CHAR' OR (VALUETYPE = 'INT' AND IS_VALID_INT(VALUE)))

so that "VALUETYPE" can take the values "CHAR" or "INT" and in the latter case, "VALUE" must hold a valid representation of an integer.

Author of SIRA_PRISE

#12 · June 21, 2020, 12:35 pm

Quote from AntC on June 21, 2020, 12:35 pm
Quote from Dave Voorhis on June 21, 2020, 11:28 am
Quote from AntC on June 21, 2020, 3:11 am
Quote from Dave Voorhis on June 20, 2020, 11:19 am

Quote from Dave Voorhis on June 20, 2020, 11:14 am

I'm not clear what you're asking in your last bullet point.

Do you mean this?

TYPE Glob UNION;

TYPE City IS {Glob POSSREP {c CHAR}};

TYPE Glob UNION; TYPE City IS {Glob POSSREP {c CHAR}};
TYPE Glob UNION;
TYPE City IS {Glob POSSREP {c CHAR}};
So this:

WRITELN City('Delft');

WRITELN 'Delft';

WRITELN TYPE_OF(City('Delft'));

WRITELN TYPE_OF('Delft');

City("Delft")

Delft

Scalar("City")

Scalar("CHARACTER")

Ok.

WRITELN City('Delft'); WRITELN 'Delft'; WRITELN TYPE_OF(City('Delft')); WRITELN TYPE_OF('Delft'); City("Delft") Delft Scalar("City") Scalar("CHARACTER") Ok.
WRITELN City('Delft');
WRITELN 'Delft';
WRITELN TYPE_OF(City('Delft'));
WRITELN TYPE_OF('Delft');

City("Delft")
Delft
Scalar("City")
Scalar("CHARACTER")

Ok.
Thanks Dave, yes that's kinda along the right lines. I'm puzzled what Glob is doing. I want only one based-on type (viz. CHAR) in the UNION, so could I name the UNION type same as the Selector? Em I think no, because TYPE City ... uses that name. In which case what is TYPE City ... doing that Glob isn't doing? Can't I go: TYPE CHAR is Glob; ?
No, you can't.

I don't think there's any use in a UNION type with a single element. There doesn't appear to be any point in having Glob, and for practical purposes I would just define TYPE City POSSREP {c CHAR}.
Then that City is not a phantom type, but merely another type with a single component. And storing a City in an attribute value in a relvar would store both the CHAR component Delft and the selector c( ).

I was merely trying to implement what you described, but perhaps I misunderstood something.

More likely it's me not understanding the IM. I guessed UNION types because of your using them to simulate tagged unions; also because the values are elements simpliciter of the based-on type. How would this go:
TYPE City UNION;
TYPE flob IS {City POSSREP {c CHAR}};    // flob and c are unused/dummy names

VAR c City;
c := City('Delft')
The point being that City('Delft') looks like a selector invocation but isn't: it's invoking TYPE City to type-annotate the CHAR value.

I thought the syntax for UNION was to follow it immediately by a embraced commalist of types in the union(?) Or is the syntax you use equivalent?

No, the Tutorial D UNION has, to my knowledge, never used an embraced commalist of types in the union.

Yes OK. That possibility is considered in DBE, then rejected.

A more realistic application might be something like this: ...

I'm well aware I'm trying to fake something. So realistic examples aren't going to achieve that.
Presuming there's a similar definition for type PName also based on CHAR but distinct from City and a function/operator Country_of( ) whose argument must be City, I want

VAR c City; // I think has to be type Glob?

c := City('Delft');

c := PName('Delft'); // rejected: ill-typed

c := 'Delft'; // i.e. CHAR rejected: ill typed

cc := Country_of(c) // cc == 'Netherlands'

cc := Country_of(PName('Delft')); // rejected: ill-typed

cc := Country_of('Delft'); // rejected: ill-typed

pc := Product_category(PName('Delft')) // pc == 'Tableware'

pc := Product_category(City('Delft')) // rejected: ill-typed

VAR c City; // I think has to be type Glob? c := City('Delft'); c := PName('Delft'); // rejected: ill-typed c := 'Delft'; // i.e. CHAR rejected: ill typed cc := Country_of(c) // cc == 'Netherlands' cc := Country_of(PName('Delft')); // rejected: ill-typed cc := Country_of('Delft'); // rejected: ill-typed pc := Product_category(PName('Delft')) // pc == 'Tableware' pc := Product_category(City('Delft')) // rejected: ill-typed
VAR c City;                             // I think has to be type Glob?
c := City('Delft');
c := PName('Delft');                    // rejected: ill-typed
c := 'Delft';                           // i.e. CHAR rejected: ill typed

cc := Country_of(c)                     // cc == 'Netherlands'
cc := Country_of(PName('Delft'));       // rejected: ill-typed
cc := Country_of('Delft');              // rejected: ill-typed

pc := Product_category(PName('Delft'))  // pc == 'Tableware'
pc := Product_category(City('Delft'))   // rejected: ill-typed
Sorry, I'm not following this but haven't looked closely because I'm in a hurry to go out. Will look again when I return.
With the above revised decl of TYPE City UNION;, that might now go OK. I suspect that c := 'Delft' and Country_of('Delft') will be type-correct. Then City is not acting as a phantom type; rather as some sort of alias for/not distinct from CHAR.

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

Quote from Dave Voorhis on June 21, 2020, 11:28 am
Quote from AntC on June 21, 2020, 3:11 am
Quote from Dave Voorhis on June 20, 2020, 11:19 am

Quote from Dave Voorhis on June 20, 2020, 11:14 am

I'm not clear what you're asking in your last bullet point.

Do you mean this?

TYPE Glob UNION;

TYPE City IS {Glob POSSREP {c CHAR}};

TYPE Glob UNION; TYPE City IS {Glob POSSREP {c CHAR}};
TYPE Glob UNION;
TYPE City IS {Glob POSSREP {c CHAR}};
So this:

WRITELN City('Delft');

WRITELN 'Delft';

WRITELN TYPE_OF(City('Delft'));

WRITELN TYPE_OF('Delft');

City("Delft")

Delft

Scalar("City")

Scalar("CHARACTER")

Ok.

WRITELN City('Delft'); WRITELN 'Delft'; WRITELN TYPE_OF(City('Delft')); WRITELN TYPE_OF('Delft'); City("Delft") Delft Scalar("City") Scalar("CHARACTER") Ok.
WRITELN City('Delft');
WRITELN 'Delft';
WRITELN TYPE_OF(City('Delft'));
WRITELN TYPE_OF('Delft');

City("Delft")
Delft
Scalar("City")
Scalar("CHARACTER")

Ok.
Thanks Dave, yes that's kinda along the right lines. I'm puzzled what Glob is doing. I want only one based-on type (viz. CHAR) in the UNION, so could I name the UNION type same as the Selector? Em I think no, because TYPE City ... uses that name. In which case what is TYPE City ... doing that Glob isn't doing? Can't I go: TYPE CHAR is Glob; ?
No, you can't.

I don't think there's any use in a UNION type with a single element. There doesn't appear to be any point in having Glob, and for practical purposes I would just define TYPE City POSSREP {c CHAR}.

Then that City is not a phantom type, but merely another type with a single component. And storing a City in an attribute value in a relvar would store both the CHAR component Delft and the selector c( ).

I was merely trying to implement what you described, but perhaps I misunderstood something.

More likely it's me not understanding the IM. I guessed UNION types because of your using them to simulate tagged unions; also because the values are elements simpliciter of the based-on type. How would this go:

TYPE City UNION;
TYPE flob IS {City POSSREP {c CHAR}};    // flob and c are unused/dummy names

VAR c City;
c := City('Delft')

The point being that City('Delft') looks like a selector invocation but isn't: it's invoking TYPE City to type-annotate the CHAR value.

I thought the syntax for UNION was to follow it immediately by a embraced commalist of types in the union(?) Or is the syntax you use equivalent?

No, the Tutorial D UNION has, to my knowledge, never used an embraced commalist of types in the union.

Yes OK. That possibility is considered in DBE, then rejected.

A more realistic application might be something like this: ...

I'm well aware I'm trying to fake something. So realistic examples aren't going to achieve that.

Presuming there's a similar definition for type PName also based on CHAR but distinct from City and a function/operator Country_of( ) whose argument must be City, I want

VAR c City; // I think has to be type Glob?

c := City('Delft');

c := PName('Delft'); // rejected: ill-typed

c := 'Delft'; // i.e. CHAR rejected: ill typed

cc := Country_of(c) // cc == 'Netherlands'

cc := Country_of(PName('Delft')); // rejected: ill-typed

cc := Country_of('Delft'); // rejected: ill-typed

pc := Product_category(PName('Delft')) // pc == 'Tableware'

pc := Product_category(City('Delft')) // rejected: ill-typed

VAR c City; // I think has to be type Glob? c := City('Delft'); c := PName('Delft'); // rejected: ill-typed c := 'Delft'; // i.e. CHAR rejected: ill typed cc := Country_of(c) // cc == 'Netherlands' cc := Country_of(PName('Delft')); // rejected: ill-typed cc := Country_of('Delft'); // rejected: ill-typed pc := Product_category(PName('Delft')) // pc == 'Tableware' pc := Product_category(City('Delft')) // rejected: ill-typed
VAR c City;                             // I think has to be type Glob?
c := City('Delft');
c := PName('Delft');                    // rejected: ill-typed
c := 'Delft';                           // i.e. CHAR rejected: ill typed

cc := Country_of(c)                     // cc == 'Netherlands'
cc := Country_of(PName('Delft'));       // rejected: ill-typed
cc := Country_of('Delft');              // rejected: ill-typed

pc := Product_category(PName('Delft'))  // pc == 'Tableware'
pc := Product_category(City('Delft'))   // rejected: ill-typed
Sorry, I'm not following this but haven't looked closely because I'm in a hurry to go out. Will look again when I return.

With the above revised decl of TYPE City UNION;, that might now go OK. I suspect that c := 'Delft' and Country_of('Delft') will be type-correct. Then City is not acting as a phantom type; rather as some sort of alias for/not distinct from CHAR.

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

#13 · June 21, 2020, 12:45 pm

Quote from Erwin on June 21, 2020, 12:34 pm

Quote from AntC on June 20, 2020, 2:58 am

So a Tutorial D/IM question:

Is it allowed to form a UNION type with only one type element?

Presumably that UNION type's name is distinct from the name of its based-on type(?)

Presumably the type still needs a tag to Select values of the UNION, even though all such values have MST of the based-on type(?)

What is the type of that tag/Selector?

Can I form a UNION type name CITY with Selector CITY that selects a CHAR? (How) is CITY('Delft') (or however you write it) distinguished from plain CHAR 'Delft'?

Allowed, probably yes because the TTM authors are generally reluctant to rule out degenerate cases merely because they're "not useful anyway". Useful, seems like no.

Yes the name must be distinct.

No, no selectors are introduced because in general union types cannot be guaranteed to have possreps that can render every single value of the union. And selectors are tied to possreps.

So, "that tag/selector" generally does not exist.

I'm too puzzled by the fifth question.

See my reply just now to Dave. Any clearer?

Oh yes, and that's of course the IM version of UNION types. If you're talking of trying to get the notional equivalent of union-types-of-the-literature outside the IM ...

No I'm abusing Tutorial D/the IM to deliberately arrive at a degenerate case of a type with a distinct type name but same set of values in the type. (Exploiting that any set is a subset of itself.) Dave seems to have declared a UNION type without any CONSTRAINT [good!] but we could always put a constraint that's always True.

#14 · June 21, 2020, 3:06 pm

Quote from Dave Voorhis on June 21, 2020, 3:06 pm
Quote from AntC on June 21, 2020, 12:35 pm
Quote from Dave Voorhis on June 21, 2020, 11:28 am
Quote from AntC on June 21, 2020, 3:11 am
Quote from Dave Voorhis on June 20, 2020, 11:19 am

Quote from Dave Voorhis on June 20, 2020, 11:14 am

I'm not clear what you're asking in your last bullet point.

Do you mean this?

TYPE Glob UNION;

TYPE City IS {Glob POSSREP {c CHAR}};

TYPE Glob UNION; TYPE City IS {Glob POSSREP {c CHAR}};
TYPE Glob UNION;
TYPE City IS {Glob POSSREP {c CHAR}};
So this:

WRITELN City('Delft');

WRITELN 'Delft';

WRITELN TYPE_OF(City('Delft'));

WRITELN TYPE_OF('Delft');

City("Delft")

Delft

Scalar("City")

Scalar("CHARACTER")

Ok.

WRITELN City('Delft'); WRITELN 'Delft'; WRITELN TYPE_OF(City('Delft')); WRITELN TYPE_OF('Delft'); City("Delft") Delft Scalar("City") Scalar("CHARACTER") Ok.
WRITELN City('Delft');
WRITELN 'Delft';
WRITELN TYPE_OF(City('Delft'));
WRITELN TYPE_OF('Delft');

City("Delft")
Delft
Scalar("City")
Scalar("CHARACTER")

Ok.
Thanks Dave, yes that's kinda along the right lines. I'm puzzled what Glob is doing. I want only one based-on type (viz. CHAR) in the UNION, so could I name the UNION type same as the Selector? Em I think no, because TYPE City ... uses that name. In which case what is TYPE City ... doing that Glob isn't doing? Can't I go: TYPE CHAR is Glob; ?
No, you can't.

I don't think there's any use in a UNION type with a single element. There doesn't appear to be any point in having Glob, and for practical purposes I would just define TYPE City POSSREP {c CHAR}.
Then that City is not a phantom type, but merely another type with a single component. And storing a City in an attribute value in a relvar would store both the CHAR component Delft and the selector c( ).
There is no selector c(). There is a selector City(CHAR), but it wouldn't be stored in the attribute value. (...?)

So I'm not sure what you mean.
I was merely trying to implement what you described, but perhaps I misunderstood something.

More likely it's me not understanding the IM. I guessed UNION types because of your using them to simulate tagged unions; also because the values are elements simpliciter of the based-on type. How would this go:

TYPE City UNION;

TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names

VAR c City;

c := City('Delft')

TYPE City UNION; TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names VAR c City; c := City('Delft')
TYPE City UNION;
TYPE flob IS {City POSSREP {c CHAR}};    // flob and c are unused/dummy names

VAR c City;
c := City('Delft')
The point being that City('Delft') looks like a selector invocation but isn't: it's invoking TYPE City to type-annotate the CHAR value.
Sorry, not following this at all.

I thought the syntax for UNION was to follow it immediately by a embraced commalist of types in the union(?) Or is the syntax you use equivalent?

No, the Tutorial D UNION has, to my knowledge, never used an embraced commalist of types in the union.

Yes OK. That possibility is considered in DBE, then rejected.

A more realistic application might be something like this: ...

I'm well aware I'm trying to fake something. So realistic examples aren't going to achieve that.

Sorry, I'm not clear what you're trying to achieve.
Presuming there's a similar definition for type PName also based on CHAR but distinct from City and a function/operator Country_of( ) whose argument must be City, I want

VAR c City; // I think has to be type Glob?

c := City('Delft');

c := PName('Delft'); // rejected: ill-typed

c := 'Delft'; // i.e. CHAR rejected: ill typed

cc := Country_of(c) // cc == 'Netherlands'

cc := Country_of(PName('Delft')); // rejected: ill-typed

cc := Country_of('Delft'); // rejected: ill-typed

pc := Product_category(PName('Delft')) // pc == 'Tableware'

pc := Product_category(City('Delft')) // rejected: ill-typed

VAR c City; // I think has to be type Glob? c := City('Delft'); c := PName('Delft'); // rejected: ill-typed c := 'Delft'; // i.e. CHAR rejected: ill typed cc := Country_of(c) // cc == 'Netherlands' cc := Country_of(PName('Delft')); // rejected: ill-typed cc := Country_of('Delft'); // rejected: ill-typed pc := Product_category(PName('Delft')) // pc == 'Tableware' pc := Product_category(City('Delft')) // rejected: ill-typed
VAR c City;                             // I think has to be type Glob?
c := City('Delft');
c := PName('Delft');                    // rejected: ill-typed
c := 'Delft';                           // i.e. CHAR rejected: ill typed

cc := Country_of(c)                     // cc == 'Netherlands'
cc := Country_of(PName('Delft'));       // rejected: ill-typed
cc := Country_of('Delft');              // rejected: ill-typed

pc := Product_category(PName('Delft'))  // pc == 'Tableware'
pc := Product_category(City('Delft'))   // rejected: ill-typed
Sorry, I'm not following this but haven't looked closely because I'm in a hurry to go out. Will look again when I return.
With the above revised decl of TYPE City UNION;, that might now go OK. I suspect that c := 'Delft' and Country_of('Delft') will be type-correct. Then City is not acting as a phantom type; rather as some sort of alias for/not distinct from CHAR.
Sorry, not following.

Where/how is Country_of(CHAR) defined?

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

Don't understand this at all, I'm afraid.

Quote from AntC on June 21, 2020, 12:35 pm
Quote from Dave Voorhis on June 21, 2020, 11:28 am
Quote from AntC on June 21, 2020, 3:11 am
Quote from Dave Voorhis on June 20, 2020, 11:19 am

Quote from Dave Voorhis on June 20, 2020, 11:14 am

I'm not clear what you're asking in your last bullet point.

Do you mean this?

TYPE Glob UNION;

TYPE City IS {Glob POSSREP {c CHAR}};

TYPE Glob UNION; TYPE City IS {Glob POSSREP {c CHAR}};
TYPE Glob UNION;
TYPE City IS {Glob POSSREP {c CHAR}};
So this:

WRITELN City('Delft');

WRITELN 'Delft';

WRITELN TYPE_OF(City('Delft'));

WRITELN TYPE_OF('Delft');

City("Delft")

Delft

Scalar("City")

Scalar("CHARACTER")

Ok.

WRITELN City('Delft'); WRITELN 'Delft'; WRITELN TYPE_OF(City('Delft')); WRITELN TYPE_OF('Delft'); City("Delft") Delft Scalar("City") Scalar("CHARACTER") Ok.
WRITELN City('Delft');
WRITELN 'Delft';
WRITELN TYPE_OF(City('Delft'));
WRITELN TYPE_OF('Delft');

City("Delft")
Delft
Scalar("City")
Scalar("CHARACTER")

Ok.
Thanks Dave, yes that's kinda along the right lines. I'm puzzled what Glob is doing. I want only one based-on type (viz. CHAR) in the UNION, so could I name the UNION type same as the Selector? Em I think no, because TYPE City ... uses that name. In which case what is TYPE City ... doing that Glob isn't doing? Can't I go: TYPE CHAR is Glob; ?
No, you can't.

I don't think there's any use in a UNION type with a single element. There doesn't appear to be any point in having Glob, and for practical purposes I would just define TYPE City POSSREP {c CHAR}.
Then that City is not a phantom type, but merely another type with a single component. And storing a City in an attribute value in a relvar would store both the CHAR component Delft and the selector c( ).

There is no selector c(). There is a selector City(CHAR), but it wouldn't be stored in the attribute value. (...?)

So I'm not sure what you mean.

I was merely trying to implement what you described, but perhaps I misunderstood something.

More likely it's me not understanding the IM. I guessed UNION types because of your using them to simulate tagged unions; also because the values are elements simpliciter of the based-on type. How would this go:

TYPE City UNION;

TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names

VAR c City;

c := City('Delft')

TYPE City UNION; TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names VAR c City; c := City('Delft')
TYPE City UNION;
TYPE flob IS {City POSSREP {c CHAR}};    // flob and c are unused/dummy names

VAR c City;
c := City('Delft')
The point being that City('Delft') looks like a selector invocation but isn't: it's invoking TYPE City to type-annotate the CHAR value.

Sorry, not following this at all.

I thought the syntax for UNION was to follow it immediately by a embraced commalist of types in the union(?) Or is the syntax you use equivalent?

No, the Tutorial D UNION has, to my knowledge, never used an embraced commalist of types in the union.

Yes OK. That possibility is considered in DBE, then rejected.

A more realistic application might be something like this: ...

I'm well aware I'm trying to fake something. So realistic examples aren't going to achieve that.

Sorry, I'm not clear what you're trying to achieve.

Presuming there's a similar definition for type PName also based on CHAR but distinct from City and a function/operator Country_of( ) whose argument must be City, I want

VAR c City; // I think has to be type Glob?

c := City('Delft');

c := PName('Delft'); // rejected: ill-typed

c := 'Delft'; // i.e. CHAR rejected: ill typed

cc := Country_of(c) // cc == 'Netherlands'

cc := Country_of(PName('Delft')); // rejected: ill-typed

cc := Country_of('Delft'); // rejected: ill-typed

pc := Product_category(PName('Delft')) // pc == 'Tableware'

pc := Product_category(City('Delft')) // rejected: ill-typed

VAR c City; // I think has to be type Glob? c := City('Delft'); c := PName('Delft'); // rejected: ill-typed c := 'Delft'; // i.e. CHAR rejected: ill typed cc := Country_of(c) // cc == 'Netherlands' cc := Country_of(PName('Delft')); // rejected: ill-typed cc := Country_of('Delft'); // rejected: ill-typed pc := Product_category(PName('Delft')) // pc == 'Tableware' pc := Product_category(City('Delft')) // rejected: ill-typed
VAR c City;                             // I think has to be type Glob?
c := City('Delft');
c := PName('Delft');                    // rejected: ill-typed
c := 'Delft';                           // i.e. CHAR rejected: ill typed

cc := Country_of(c)                     // cc == 'Netherlands'
cc := Country_of(PName('Delft'));       // rejected: ill-typed
cc := Country_of('Delft');              // rejected: ill-typed

pc := Product_category(PName('Delft'))  // pc == 'Tableware'
pc := Product_category(City('Delft'))   // rejected: ill-typed
Sorry, I'm not following this but haven't looked closely because I'm in a hurry to go out. Will look again when I return.
With the above revised decl of TYPE City UNION;, that might now go OK. I suspect that c := 'Delft' and Country_of('Delft') will be type-correct. Then City is not acting as a phantom type; rather as some sort of alias for/not distinct from CHAR.

Sorry, not following.

Where/how is Country_of(CHAR) defined?

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

Don't understand this at all, I'm afraid.

I'm the forum administrator and lead developer of Rel. Email me at dave@armchair.mb.ca with the Subject 'TTM Forum'. Download Rel from https://reldb.org

#15 · June 22, 2020, 4:00 am

Quote from AntC on June 22, 2020, 4:00 am
OK I'll give up. Not worth pursuing.
Quote from Dave Voorhis on June 21, 2020, 3:06 pm
Quote from AntC on June 21, 2020, 12:35 pm
Quote from Dave Voorhis on June 21, 2020, 11:28 am
Quote from AntC on June 21, 2020, 3:11 am
Quote from Dave Voorhis on June 20, 2020, 11:19 am

Quote from Dave Voorhis on June 20, 2020, 11:14 am

I'm not clear what you're asking in your last bullet point.

Do you mean this?

TYPE Glob UNION;

TYPE City IS {Glob POSSREP {c CHAR}};

TYPE Glob UNION; TYPE City IS {Glob POSSREP {c CHAR}};
TYPE Glob UNION;
TYPE City IS {Glob POSSREP {c CHAR}};
So this:

WRITELN City('Delft');

WRITELN 'Delft';

WRITELN TYPE_OF(City('Delft'));

WRITELN TYPE_OF('Delft');

City("Delft")

Delft

Scalar("City")

Scalar("CHARACTER")

Ok.

WRITELN City('Delft'); WRITELN 'Delft'; WRITELN TYPE_OF(City('Delft')); WRITELN TYPE_OF('Delft'); City("Delft") Delft Scalar("City") Scalar("CHARACTER") Ok.
WRITELN City('Delft');
WRITELN 'Delft';
WRITELN TYPE_OF(City('Delft'));
WRITELN TYPE_OF('Delft');

City("Delft")
Delft
Scalar("City")
Scalar("CHARACTER")

Ok.
Thanks Dave, yes that's kinda along the right lines. I'm puzzled what Glob is doing. I want only one based-on type (viz. CHAR) in the UNION, so could I name the UNION type same as the Selector? Em I think no, because TYPE City ... uses that name. In which case what is TYPE City ... doing that Glob isn't doing? Can't I go: TYPE CHAR is Glob; ?
No, you can't.

I don't think there's any use in a UNION type with a single element. There doesn't appear to be any point in having Glob, and for practical purposes I would just define TYPE City POSSREP {c CHAR}.
Then that City is not a phantom type, but merely another type with a single component. And storing a City in an attribute value in a relvar would store both the CHAR component Delft and the selector c( ).
There is no selector c(). There is a selector City(CHAR), but it wouldn't be stored in the attribute value. (...?)

So I'm not sure what you mean.
I was merely trying to implement what you described, but perhaps I misunderstood something.

More likely it's me not understanding the IM. I guessed UNION types because of your using them to simulate tagged unions; also because the values are elements simpliciter of the based-on type. How would this go:

TYPE City UNION;

TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names

VAR c City;

c := City('Delft')

TYPE City UNION; TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names VAR c City; c := City('Delft')
TYPE City UNION;
TYPE flob IS {City POSSREP {c CHAR}};    // flob and c are unused/dummy names

VAR c City;
c := City('Delft')
The point being that City('Delft') looks like a selector invocation but isn't: it's invoking TYPE City to type-annotate the CHAR value.
Sorry, not following this at all.

I thought the syntax for UNION was to follow it immediately by a embraced commalist of types in the union(?) Or is the syntax you use equivalent?

No, the Tutorial D UNION has, to my knowledge, never used an embraced commalist of types in the union.

Yes OK. That possibility is considered in DBE, then rejected.

A more realistic application might be something like this: ...

I'm well aware I'm trying to fake something. So realistic examples aren't going to achieve that.

Sorry, I'm not clear what you're trying to achieve.
Presuming there's a similar definition for type PName also based on CHAR but distinct from City and a function/operator Country_of( ) whose argument must be City, I want

VAR c City; // I think has to be type Glob?

c := City('Delft');

c := PName('Delft'); // rejected: ill-typed

c := 'Delft'; // i.e. CHAR rejected: ill typed

cc := Country_of(c) // cc == 'Netherlands'

cc := Country_of(PName('Delft')); // rejected: ill-typed

cc := Country_of('Delft'); // rejected: ill-typed

pc := Product_category(PName('Delft')) // pc == 'Tableware'

pc := Product_category(City('Delft')) // rejected: ill-typed

VAR c City; // I think has to be type Glob? c := City('Delft'); c := PName('Delft'); // rejected: ill-typed c := 'Delft'; // i.e. CHAR rejected: ill typed cc := Country_of(c) // cc == 'Netherlands' cc := Country_of(PName('Delft')); // rejected: ill-typed cc := Country_of('Delft'); // rejected: ill-typed pc := Product_category(PName('Delft')) // pc == 'Tableware' pc := Product_category(City('Delft')) // rejected: ill-typed
VAR c City;                             // I think has to be type Glob?
c := City('Delft');
c := PName('Delft');                    // rejected: ill-typed
c := 'Delft';                           // i.e. CHAR rejected: ill typed

cc := Country_of(c)                     // cc == 'Netherlands'
cc := Country_of(PName('Delft'));       // rejected: ill-typed
cc := Country_of('Delft');              // rejected: ill-typed

pc := Product_category(PName('Delft'))  // pc == 'Tableware'
pc := Product_category(City('Delft'))   // rejected: ill-typed
Sorry, I'm not following this but haven't looked closely because I'm in a hurry to go out. Will look again when I return.
With the above revised decl of TYPE City UNION;, that might now go OK. I suspect that c := 'Delft' and Country_of('Delft') will be type-correct. Then City is not acting as a phantom type; rather as some sort of alias for/not distinct from CHAR.
Sorry, not following.

Where/how is Country_of(CHAR) defined?

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

Don't understand this at all, I'm afraid.

OK I'll give up. Not worth pursuing.

Quote from Dave Voorhis on June 21, 2020, 3:06 pm
Quote from AntC on June 21, 2020, 12:35 pm
Quote from Dave Voorhis on June 21, 2020, 11:28 am
Quote from AntC on June 21, 2020, 3:11 am
Quote from Dave Voorhis on June 20, 2020, 11:19 am

Quote from Dave Voorhis on June 20, 2020, 11:14 am

I'm not clear what you're asking in your last bullet point.

Do you mean this?

TYPE Glob UNION;

TYPE City IS {Glob POSSREP {c CHAR}};

TYPE Glob UNION; TYPE City IS {Glob POSSREP {c CHAR}};
TYPE Glob UNION;
TYPE City IS {Glob POSSREP {c CHAR}};
So this:

WRITELN City('Delft');

WRITELN 'Delft';

WRITELN TYPE_OF(City('Delft'));

WRITELN TYPE_OF('Delft');

City("Delft")

Delft

Scalar("City")

Scalar("CHARACTER")

Ok.

WRITELN City('Delft'); WRITELN 'Delft'; WRITELN TYPE_OF(City('Delft')); WRITELN TYPE_OF('Delft'); City("Delft") Delft Scalar("City") Scalar("CHARACTER") Ok.
WRITELN City('Delft');
WRITELN 'Delft';
WRITELN TYPE_OF(City('Delft'));
WRITELN TYPE_OF('Delft');

City("Delft")
Delft
Scalar("City")
Scalar("CHARACTER")

Ok.
Thanks Dave, yes that's kinda along the right lines. I'm puzzled what Glob is doing. I want only one based-on type (viz. CHAR) in the UNION, so could I name the UNION type same as the Selector? Em I think no, because TYPE City ... uses that name. In which case what is TYPE City ... doing that Glob isn't doing? Can't I go: TYPE CHAR is Glob; ?
No, you can't.

I don't think there's any use in a UNION type with a single element. There doesn't appear to be any point in having Glob, and for practical purposes I would just define TYPE City POSSREP {c CHAR}.
Then that City is not a phantom type, but merely another type with a single component. And storing a City in an attribute value in a relvar would store both the CHAR component Delft and the selector c( ).
There is no selector c(). There is a selector City(CHAR), but it wouldn't be stored in the attribute value. (...?)

So I'm not sure what you mean.
I was merely trying to implement what you described, but perhaps I misunderstood something.

More likely it's me not understanding the IM. I guessed UNION types because of your using them to simulate tagged unions; also because the values are elements simpliciter of the based-on type. How would this go:

TYPE City UNION;

TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names

VAR c City;

c := City('Delft')

TYPE City UNION; TYPE flob IS {City POSSREP {c CHAR}}; // flob and c are unused/dummy names VAR c City; c := City('Delft')
TYPE City UNION;
TYPE flob IS {City POSSREP {c CHAR}};    // flob and c are unused/dummy names

VAR c City;
c := City('Delft')
The point being that City('Delft') looks like a selector invocation but isn't: it's invoking TYPE City to type-annotate the CHAR value.
Sorry, not following this at all.

I thought the syntax for UNION was to follow it immediately by a embraced commalist of types in the union(?) Or is the syntax you use equivalent?

No, the Tutorial D UNION has, to my knowledge, never used an embraced commalist of types in the union.

Yes OK. That possibility is considered in DBE, then rejected.

A more realistic application might be something like this: ...

I'm well aware I'm trying to fake something. So realistic examples aren't going to achieve that.

Sorry, I'm not clear what you're trying to achieve.
Presuming there's a similar definition for type PName also based on CHAR but distinct from City and a function/operator Country_of( ) whose argument must be City, I want

VAR c City; // I think has to be type Glob?

c := City('Delft');

c := PName('Delft'); // rejected: ill-typed

c := 'Delft'; // i.e. CHAR rejected: ill typed

cc := Country_of(c) // cc == 'Netherlands'

cc := Country_of(PName('Delft')); // rejected: ill-typed

cc := Country_of('Delft'); // rejected: ill-typed

pc := Product_category(PName('Delft')) // pc == 'Tableware'

pc := Product_category(City('Delft')) // rejected: ill-typed

VAR c City; // I think has to be type Glob? c := City('Delft'); c := PName('Delft'); // rejected: ill-typed c := 'Delft'; // i.e. CHAR rejected: ill typed cc := Country_of(c) // cc == 'Netherlands' cc := Country_of(PName('Delft')); // rejected: ill-typed cc := Country_of('Delft'); // rejected: ill-typed pc := Product_category(PName('Delft')) // pc == 'Tableware' pc := Product_category(City('Delft')) // rejected: ill-typed
VAR c City;                             // I think has to be type Glob?
c := City('Delft');
c := PName('Delft');                    // rejected: ill-typed
c := 'Delft';                           // i.e. CHAR rejected: ill typed

cc := Country_of(c)                     // cc == 'Netherlands'
cc := Country_of(PName('Delft'));       // rejected: ill-typed
cc := Country_of('Delft');              // rejected: ill-typed

pc := Product_category(PName('Delft'))  // pc == 'Tableware'
pc := Product_category(City('Delft'))   // rejected: ill-typed
Sorry, I'm not following this but haven't looked closely because I'm in a hurry to go out. Will look again when I return.
With the above revised decl of TYPE City UNION;, that might now go OK. I suspect that c := 'Delft' and Country_of('Delft') will be type-correct. Then City is not acting as a phantom type; rather as some sort of alias for/not distinct from CHAR.
Sorry, not following.

Where/how is Country_of(CHAR) defined?

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

Don't understand this at all, I'm afraid.

#16 · June 22, 2020, 12:20 pm

Quote from Erwin on June 22, 2020, 12:20 pm

Quote from AntC on June 21, 2020, 12:35 pm

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

TTM sans IM already has what it takes to achieve that (imo). Just declare types PName and City. They will be distinct by the very act of doing so.

Now all that needs to be resolved is getting the system to understand that the 'Delft' in PName() is in fact PNAME(PNAME(STRING(DELFT))) and the 'Delft' in City() is in fact CITY(CITY(STRING(DELFT))).

In which :

the outermost PNAME() and CITY() denote the fact that there's a value selector for type PNAME resp. CITY being invoked. Call it "selector name" if you wish.

the PNAME() AND CITY() nested within denote the fact that the selector corresponding to the possrep [supposedly] named PNAME resp. CITY is being invoked.

The STRING() denotes the fact that the [sole] argument to the respective and distinct selectors being invoked is the string argument/value indicated.

DELFT denotes the actual string value that is the input to the string value selector that produces the value that is input to the PNAME resp. CITY selector invoked.

Now *doing* that requires "outside-in" compilation because the system needs to find the right mapping between the PName/City Attribute name (NOT typename, NOT selector name !!!) and the sole string argument that is given to the invocation. Getting that done requires :

that a declared type is available, or can be inferred from context, for the attribute in question.

that that type have a ***unique*** selector (across all of its existing possreps) whose invocation signature (the ordered list of parameter type declarations) is equal to "one single value of type string".

That said, my first response is thus that you don't need the IM or union types to achieve what you [seem to] want.

***Within*** the IM, I believe there is a stated requirement that for types that are in a subtype/supertype relationship wrt one another, it ***must*** be a PROPER subtype/PROPER supertype relationship, with an acknowledgement that the system can never be supposed to verify that, so it's the type designer's responsibility.

So all that leaves you with for "distinct types, same value" is "impossible, not allowed". Except for concepts such as type name aliases, but there's hard time defending that such a notion yields "distinct types".

So that said, my second response is that you seem to be after a type system that "recognises" ("acknowledges") in some way the equality/"sameness" of the "individual" 1 in the (distinct) values INT(1) and, say, BIGINT(1). TTM has never gone there and the authors have never gone any farther that observing this theoretical possibility in one of the DBE chapters (which is where I got the term "individual" from).

Quote from AntC on June 21, 2020, 12:35 pm

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

TTM sans IM already has what it takes to achieve that (imo). Just declare types PName and City. They will be distinct by the very act of doing so.

Now all that needs to be resolved is getting the system to understand that the 'Delft' in PName() is in fact PNAME(PNAME(STRING(DELFT))) and the 'Delft' in City() is in fact CITY(CITY(STRING(DELFT))).

In which :

the outermost PNAME() and CITY() denote the fact that there's a value selector for type PNAME resp. CITY being invoked. Call it "selector name" if you wish.
the PNAME() AND CITY() nested within denote the fact that the selector corresponding to the possrep [supposedly] named PNAME resp. CITY is being invoked.
The STRING() denotes the fact that the [sole] argument to the respective and distinct selectors being invoked is the string argument/value indicated.
DELFT denotes the actual string value that is the input to the string value selector that produces the value that is input to the PNAME resp. CITY selector invoked.

Now *doing* that requires "outside-in" compilation because the system needs to find the right mapping between the PName/City Attribute name (NOT typename, NOT selector name !!!) and the sole string argument that is given to the invocation. Getting that done requires :

that a declared type is available, or can be inferred from context, for the attribute in question.
that that type have a ***unique*** selector (across all of its existing possreps) whose invocation signature (the ordered list of parameter type declarations) is equal to "one single value of type string".

That said, my first response is thus that you don't need the IM or union types to achieve what you [seem to] want.

***Within*** the IM, I believe there is a stated requirement that for types that are in a subtype/supertype relationship wrt one another, it ***must*** be a PROPER subtype/PROPER supertype relationship, with an acknowledgement that the system can never be supposed to verify that, so it's the type designer's responsibility.

So all that leaves you with for "distinct types, same value" is "impossible, not allowed". Except for concepts such as type name aliases, but there's hard time defending that such a notion yields "distinct types".

So that said, my second response is that you seem to be after a type system that "recognises" ("acknowledges") in some way the equality/"sameness" of the "individual" 1 in the (distinct) values INT(1) and, say, BIGINT(1). TTM has never gone there and the authors have never gone any farther that observing this theoretical possibility in one of the DBE chapters (which is where I got the term "individual" from).

Author of SIRA_PRISE

#17 · June 23, 2020, 6:29 am

Quote from AntC on June 23, 2020, 6:29 am

Quote from Erwin on June 22, 2020, 12:20 pm

Quote from AntC on June 21, 2020, 12:35 pm

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

TTM sans IM already has what it takes to achieve that (imo). Just declare types PName and City. They will be distinct by the very act of doing so.

Now all that needs to be resolved is getting the system to understand that the 'Delft' in PName() is in fact PNAME(PNAME(STRING(DELFT))) and the 'Delft' in City() is in fact CITY(CITY(STRING(DELFT))).

No, that doesn't achieve what I want; and it suffers from excessive circumlocution. The point of 'phantom types' is there's a lightweight locution, just enough to distinguish PNames from Citys at the type level, and not elsewhere. (Also to say P#(10) is just enough distinguished from Int(10) to make it a type error to call arithmetic operations on P#s.)

To try to put it in TTM terms -- although I risk compromising the formal behaviour:

Instead of RM Pre 1: "A scalar data type (scalar type for short) is a named set of scalar values (scalars for short). Given an
arbitrary pair of distinct scalar types named T1 and T2, respectively, with corresponding sets of scalar
values S1 and S2, respectively, the names T1 and T2 shall be distinct and the sets S1 and S2 shall be
disjoint; in other words, two scalar types shall be equal—i.e., the same type—if and only if they have the
same name (and therefore the same set of values)."

Say: "A scalar data type (scalar type for short) is a named set of scalar values (scalars for short). Given an
arbitrary pair of distinct scalar types named T1 and T2, respectively, with corresponding sets of scalar
values S1 and S2, respectively, the names T1 and T2 shall be distinct and the sets S1 and S2" need not be
disjoint nor even distinct; "in other words, two scalar types shall be equal—i.e., the same type—if and only if they have the
same name (and therefore the same set of values)." Two scalar types shall be distinct if and only if they have distinct names (irrespective of set of values).

Hmm hmm perhaps instead of `values S1, S2' that should say 'appearance of/PossRep for values S1, S2' -- but of course TTM hasn't defined 'PossRep' as at RM Pre 1.

In which :

the outermost PNAME() and CITY() denote the fact that there's a value selector for type PNAME resp. CITY being invoked. Call it "selector name" if you wish.

the PNAME() AND CITY() nested within denote the fact that the selector corresponding to the possrep [supposedly] named PNAME resp. CITY is being invoked.

The STRING() denotes the fact that the [sole] argument to the respective and distinct selectors being invoked is the string argument/value indicated.

DELFT denotes the actual string value that is the input to the string value selector that produces the value that is input to the PNAME resp. CITY selector invoked.

Yeah. I have never understood why TTM sans IM needs to both use distinct types for PName vs City and then tag them with distinct attribute names.

Now *doing* that requires "outside-in" compilation because the system needs to find the right mapping between the PName/City Attribute name (NOT typename, NOT selector name !!!) and the sole string argument that is given to the invocation. Getting that done requires :

that a declared type is available, or can be inferred from context, for the attribute in question.

that that type have a ***unique*** selector (across all of its existing possreps) whose invocation signature (the ordered list of parameter type declarations) is equal to "one single value of type string".

We only need one place to differentiate the (type or attribute name) for values of the same base type. We could even say something like: values of system-supplied types cannot stand alone as attribute values, they must be wrapped in a (type or attribute name). And we could do that syntactically within TUP{ }.

Also I've never understood your fear of "outside-in" compilation. It's just a particular strategy for type inference, which makes it more determinate than Robinson's unification algorithm -- which essentially suffers combinatorial explosion.

That said, my first response is thus that you don't need the IM or union types to achieve what you [seem to] want.

I want 'phantom types': a lightweight locution at type level only over base types; given TTM doesn't support that, I'm looking how I can cheat via the IM.

***Within*** the IM, I believe there is a stated requirement that for types that are in a subtype/supertype relationship wrt one another, it ***must*** be a PROPER subtype/PROPER supertype relationship, with an acknowledgement that the system can never be supposed to verify that, so it's the type designer's responsibility.

Seems Rel doesn't comply, from Dave's experiment. Anyway it's easy to evade that: PName has the same set of values as CHAR except for snipping away one value that can't possibly be a PName; likewise City can exclude some arbitrary non-City CHAR value.

So all that leaves you with for "distinct types, same value" is "impossible, not allowed". Except for concepts such as type name aliases, but there's hard time defending that such a notion yields "distinct types".

No: type aliases are definitely a different thing entirely: their whole purpose is to be a shorthand for exactly the same type. (I want them too BTW, but they won't answer this need.)

So that said, my second response is that you seem to be after a type system that "recognises" ("acknowledges") in some way the equality/"sameness" of the "individual" 1 in the (distinct) values INT(1) and, say, BIGINT(1).

No: Those have a different PhysRep. Not an example. Even less (contra DBE Ch 22) do I want to tangle up INT(1) with RAT(1). What I do want to do is say bare 1 as a literal appearing in program text is ambiguous as to what type denotes[**], so the source context/type inference must disambiguate.

[**] that ambiguity is entirely consistent with my revised wording for RM Pre 1 above.

TTM has never gone there and the authors have never gone any farther that observing this theoretical possibility in one of the DBE chapters (which is where I got the term "individual" from).

I want to exploit the "sameness" in the implementation: the compilation system knows that the PhysRep for these "individual"s (P#( ), Weight( ), Status( ), INT( )) is the same; and knows that if you want to apply (say) arithmetic operations to the value inside Status(10), CAST_AS_INT( ) is a null op, and CAST_AS_Status( ) of the result is also a null op. That's particularly important when you're mapping some operation over a million tuples.

Quote from Erwin on June 22, 2020, 12:20 pm

Quote from AntC on June 21, 2020, 12:35 pm

I'm trying to get to TUPLE{ P#(10), PName('Delft'), City('Delft'), Weight(10) } in which the UNION type names/pseudo-selectors acting as specifiers are sufficient to say there's four values of four distinct types, so we have four attributes.

TTM sans IM already has what it takes to achieve that (imo). Just declare types PName and City. They will be distinct by the very act of doing so.

Now all that needs to be resolved is getting the system to understand that the 'Delft' in PName() is in fact PNAME(PNAME(STRING(DELFT))) and the 'Delft' in City() is in fact CITY(CITY(STRING(DELFT))).

No, that doesn't achieve what I want; and it suffers from excessive circumlocution. The point of 'phantom types' is there's a lightweight locution, just enough to distinguish PNames from Citys at the type level, and not elsewhere. (Also to say P#(10) is just enough distinguished from Int(10) to make it a type error to call arithmetic operations on P#s.)

To try to put it in TTM terms -- although I risk compromising the formal behaviour:

Instead of RM Pre 1: "A scalar data type (scalar type for short) is a named set of scalar values (scalars for short). Given an
arbitrary pair of distinct scalar types named T1 and T2, respectively, with corresponding sets of scalar
values S1 and S2, respectively, the names T1 and T2 shall be distinct and the sets S1 and S2 shall be
disjoint; in other words, two scalar types shall be equal—i.e., the same type—if and only if they have the
same name (and therefore the same set of values)."
Say: "A scalar data type (scalar type for short) is a named set of scalar values (scalars for short). Given an
arbitrary pair of distinct scalar types named T1 and T2, respectively, with corresponding sets of scalar
values S1 and S2, respectively, the names T1 and T2 shall be distinct and the sets S1 and S2" need not be
disjoint nor even distinct; "in other words, two scalar types shall be equal—i.e., the same type—if and only if they have the
same name (and therefore the same set of values)." Two scalar types shall be distinct if and only if they have distinct names (irrespective of set of values).

Hmm hmm perhaps instead of `values S1, S2' that should say 'appearance of/PossRep for values S1, S2' -- but of course TTM hasn't defined 'PossRep' as at RM Pre 1.

In which :

the outermost PNAME() and CITY() denote the fact that there's a value selector for type PNAME resp. CITY being invoked. Call it "selector name" if you wish.

the PNAME() AND CITY() nested within denote the fact that the selector corresponding to the possrep [supposedly] named PNAME resp. CITY is being invoked.

The STRING() denotes the fact that the [sole] argument to the respective and distinct selectors being invoked is the string argument/value indicated.

DELFT denotes the actual string value that is the input to the string value selector that produces the value that is input to the PNAME resp. CITY selector invoked.

Yeah. I have never understood why TTM sans IM needs to both use distinct types for PName vs City and then tag them with distinct attribute names.

Now *doing* that requires "outside-in" compilation because the system needs to find the right mapping between the PName/City Attribute name (NOT typename, NOT selector name !!!) and the sole string argument that is given to the invocation. Getting that done requires :

that a declared type is available, or can be inferred from context, for the attribute in question.

that that type have a ***unique*** selector (across all of its existing possreps) whose invocation signature (the ordered list of parameter type declarations) is equal to "one single value of type string".

We only need one place to differentiate the (type or attribute name) for values of the same base type. We could even say something like: values of system-supplied types cannot stand alone as attribute values, they must be wrapped in a (type or attribute name). And we could do that syntactically within TUP{ }.

Also I've never understood your fear of "outside-in" compilation. It's just a particular strategy for type inference, which makes it more determinate than Robinson's unification algorithm -- which essentially suffers combinatorial explosion.

That said, my first response is thus that you don't need the IM or union types to achieve what you [seem to] want.

I want 'phantom types': a lightweight locution at type level only over base types; given TTM doesn't support that, I'm looking how I can cheat via the IM.

***Within*** the IM, I believe there is a stated requirement that for types that are in a subtype/supertype relationship wrt one another, it ***must*** be a PROPER subtype/PROPER supertype relationship, with an acknowledgement that the system can never be supposed to verify that, so it's the type designer's responsibility.

Seems Rel doesn't comply, from Dave's experiment. Anyway it's easy to evade that: PName has the same set of values as CHAR except for snipping away one value that can't possibly be a PName; likewise City can exclude some arbitrary non-City CHAR value.

So all that leaves you with for "distinct types, same value" is "impossible, not allowed". Except for concepts such as type name aliases, but there's hard time defending that such a notion yields "distinct types".

No: type aliases are definitely a different thing entirely: their whole purpose is to be a shorthand for exactly the same type. (I want them too BTW, but they won't answer this need.)

So that said, my second response is that you seem to be after a type system that "recognises" ("acknowledges") in some way the equality/"sameness" of the "individual" 1 in the (distinct) values INT(1) and, say, BIGINT(1).

No: Those have a different PhysRep. Not an example. Even less (contra DBE Ch 22) do I want to tangle up INT(1) with RAT(1). What I do want to do is say bare 1 as a literal appearing in program text is ambiguous as to what type denotes[**], so the source context/type inference must disambiguate.

[**] that ambiguity is entirely consistent with my revised wording for RM Pre 1 above.

TTM has never gone there and the authors have never gone any farther that observing this theoretical possibility in one of the DBE chapters (which is where I got the term "individual" from).

I want to exploit the "sameness" in the implementation: the compilation system knows that the PhysRep for these "individual"s (P#( ), Weight( ), Status( ), INT( )) is the same; and knows that if you want to apply (say) arithmetic operations to the value inside Status(10), CAST_AS_INT( ) is a null op, and CAST_AS_Status( ) of the result is also a null op. That's particularly important when you're mapping some operation over a million tuples.

#18 · June 23, 2020, 7:54 am

Quote from Erwin on June 23, 2020, 7:54 am

Quote from AntC on June 23, 2020, 6:29 am

In which :

the outermost PNAME() and CITY() denote the fact that there's a value selector for type PNAME resp. CITY being invoked. Call it "selector name" if you wish.

the PNAME() AND CITY() nested within denote the fact that the selector corresponding to the possrep [supposedly] named PNAME resp. CITY is being invoked.

The STRING() denotes the fact that the [sole] argument to the respective and distinct selectors being invoked is the string argument/value indicated.

DELFT denotes the actual string value that is the input to the string value selector that produces the value that is input to the PNAME resp. CITY selector invoked.

Yeah. I have never understood why TTM sans IM needs to both use distinct types for PName vs City and then tag them with distinct attribute names.

It doesn't do that and it doesn't need to. And please use correct terminology. The names of the things that make up a possrep are "component names", not attribute names.

Current languages already have "multiple possreps". Integers can be written as "16" as well as "0x0010". Chars can be written as ' ' as well as '\u0020'. Calendar dates have all kinds of rendition. So this multiple possrep things is plain and simple a requirement inherited from what currently existing languaes already do.

Now can a language with a truly open type system employ those same kinds of syntactic tricks with hieroglyphs for every type (also the user-defined ones, the "plug-in" ones) ? Achieving that requires there be a device in the type definition language that says to the compiler "my syntactic trick is regexes of the form "§.*§" " or some such. And then we need an internet registrar of syntactic tricks so two type definers don't both use the very same syntactic trick for their distinct types. So we might need to introduce namespaces to distinguish otherwise indistinguishable syntactic tricks. Boy, am I going to love that language ... So I think, no it can't, to answer my original question.

So what you do is you give things a name. So we get multiple possreps distinguished by name.

And a D can perfectly have
TYPE PNAME POSSREP T (CHAR TV) ;
TYPE CITY POSSREP T (CHAR TV) ;
(PS ***Tutorial D*** cannot have that because it has made a choice to use the possrep name as the syntactic device to identify its selector invocations, hence CARTESIAN (and every other possrep name of every other type) must be unique across all types, but that is Tutorial D, not TTM.)

(Continued)

Quote from AntC on June 23, 2020, 6:29 am

In which :

the outermost PNAME() and CITY() denote the fact that there's a value selector for type PNAME resp. CITY being invoked. Call it "selector name" if you wish.

the PNAME() AND CITY() nested within denote the fact that the selector corresponding to the possrep [supposedly] named PNAME resp. CITY is being invoked.

The STRING() denotes the fact that the [sole] argument to the respective and distinct selectors being invoked is the string argument/value indicated.

DELFT denotes the actual string value that is the input to the string value selector that produces the value that is input to the PNAME resp. CITY selector invoked.

Yeah. I have never understood why TTM sans IM needs to both use distinct types for PName vs City and then tag them with distinct attribute names.

It doesn't do that and it doesn't need to. And please use correct terminology. The names of the things that make up a possrep are "component names", not attribute names.

Current languages already have "multiple possreps". Integers can be written as "16" as well as "0x0010". Chars can be written as ' ' as well as '\u0020'. Calendar dates have all kinds of rendition. So this multiple possrep things is plain and simple a requirement inherited from what currently existing languaes already do.

Now can a language with a truly open type system employ those same kinds of syntactic tricks with hieroglyphs for every type (also the user-defined ones, the "plug-in" ones) ? Achieving that requires there be a device in the type definition language that says to the compiler "my syntactic trick is regexes of the form "§.*§" " or some such. And then we need an internet registrar of syntactic tricks so two type definers don't both use the very same syntactic trick for their distinct types. So we might need to introduce namespaces to distinguish otherwise indistinguishable syntactic tricks. Boy, am I going to love that language ... So I think, no it can't, to answer my original question.

So what you do is you give things a name. So we get multiple possreps distinguished by name.

And a D can perfectly have

TYPE PNAME POSSREP T (CHAR TV) ;
TYPE CITY POSSREP T (CHAR TV) ;

(PS ***Tutorial D*** cannot have that because it has made a choice to use the possrep name as the syntactic device to identify its selector invocations, hence CARTESIAN (and every other possrep name of every other type) must be unique across all types, but that is Tutorial D, not TTM.)

(Continued)

Author of SIRA_PRISE

#19 · June 23, 2020, 8:21 am

Quote from Erwin on June 23, 2020, 8:21 am

Quote from AntC on June 23, 2020, 6:29 am

Quote from Erwin on June 22, 2020, 12:20 pm

Now *doing* that requires "outside-in" compilation because the system needs to find the right mapping between the PName/City Attribute name (NOT typename, NOT selector name !!!) and the sole string argument that is given to the invocation. Getting that done requires :

that a declared type is available, or can be inferred from context, for the attribute in question.

that that type have a ***unique*** selector (across all of its existing possreps) whose invocation signature (the ordered list of parameter type declarations) is equal to "one single value of type string".

We only need one place to differentiate the (type or attribute name) for values of the same base type. We could even say something like: values of system-supplied types cannot stand alone as attribute values, they must be wrapped in a (type or attribute name). And we could do that syntactically within TUP{ }.

Also I've never understood your fear of "outside-in" compilation. It's just a particular strategy for type inference, which makes it more determinate than Robinson's unification algorithm -- which essentially suffers combinatorial explosion.

"We only need one place to differentiate ..." : that's the kind of hollow manipulative slogan that no one can disagree with because if you do disagree then the obvious reply is "so you think we need more than one place to differentiate ?". But fortunately slogans mean nothing so there is no need to respond. Except perhaps to add that yes it is, and which place you make that is YOUR choice as the designer of YOUR D.

Well OF COURSE "values of system-supplied types cannot stand alone as attribute values" because if they truly are an attribute value then they are part of a tuple which by definition means they no longer "stand alone". The follow-up of that phrase seems to betray that you are taking not about the value, but about the syntax for denoting it. So you are prescribing syntax. No interest in discussing that.

And I have no such thing as "fear of outside-in compilation". I ***implemented it***. I got to the point where I could write BAR(1) where "BAR" is the name of an attribute in a tuple being selected and "1" is the textual rendition of the integer number one that is to be the attribute value for the BAR attribute in the tuple being selected. Context allowing, of course. And it doesn't stop me from realizing that what is really going on is very much indeed BAR(INT(DEC(STRING(1)))). INT is the typename identifying the type name. DEC is the possrep name identifying the DEC selector. STRING introduces the selector for the string argument value fed to the DEC selector. And the 1, well I suppose you understand that one.

Quote from AntC on June 23, 2020, 6:29 am

Quote from Erwin on June 22, 2020, 12:20 pm

Now *doing* that requires "outside-in" compilation because the system needs to find the right mapping between the PName/City Attribute name (NOT typename, NOT selector name !!!) and the sole string argument that is given to the invocation. Getting that done requires :

that a declared type is available, or can be inferred from context, for the attribute in question.

that that type have a ***unique*** selector (across all of its existing possreps) whose invocation signature (the ordered list of parameter type declarations) is equal to "one single value of type string".

We only need one place to differentiate the (type or attribute name) for values of the same base type. We could even say something like: values of system-supplied types cannot stand alone as attribute values, they must be wrapped in a (type or attribute name). And we could do that syntactically within TUP{ }.

Also I've never understood your fear of "outside-in" compilation. It's just a particular strategy for type inference, which makes it more determinate than Robinson's unification algorithm -- which essentially suffers combinatorial explosion.

"We only need one place to differentiate ..." : that's the kind of hollow manipulative slogan that no one can disagree with because if you do disagree then the obvious reply is "so you think we need more than one place to differentiate ?". But fortunately slogans mean nothing so there is no need to respond. Except perhaps to add that yes it is, and which place you make that is YOUR choice as the designer of YOUR D.

Well OF COURSE "values of system-supplied types cannot stand alone as attribute values" because if they truly are an attribute value then they are part of a tuple which by definition means they no longer "stand alone". The follow-up of that phrase seems to betray that you are taking not about the value, but about the syntax for denoting it. So you are prescribing syntax. No interest in discussing that.

And I have no such thing as "fear of outside-in compilation". I ***implemented it***. I got to the point where I could write BAR(1) where "BAR" is the name of an attribute in a tuple being selected and "1" is the textual rendition of the integer number one that is to be the attribute value for the BAR attribute in the tuple being selected. Context allowing, of course. And it doesn't stop me from realizing that what is really going on is very much indeed BAR(INT(DEC(STRING(1)))). INT is the typename identifying the type name. DEC is the possrep name identifying the DEC selector. STRING introduces the selector for the string argument value fed to the DEC selector. And the 1, well I suppose you understand that one.

Author of SIRA_PRISE

#20 · June 23, 2020, 8:34 am

Quote from AntC on June 23, 2020, 6:29 am

Quote from Erwin on June 22, 2020, 12:20 pm

So that said, my second response is that you seem to be after a type system that "recognises" ("acknowledges") in some way the equality/"sameness" of the "individual" 1 in the (distinct) values INT(1) and, say, BIGINT(1).

No: Those have a different PhysRep. Not an example. Even less (contra DBE Ch 22) do I want to tangle up INT(1) with RAT(1). What I do want to do is say bare 1 as a literal appearing in program text is ambiguous as to what type denotes[**], so the source context/type inference must disambiguate.

[**] that ambiguity is entirely consistent with my revised wording for RM Pre 1 above.

"Different physrep" is not an answer and it shows you don't understand the nature of type systems as systems of [manipulation of] ***abstract*** values.

What the Physrep looks like ***should be left to the type designer/definer***. As a consequence, you cannot know what the physrep is, and as an ensuing consequence, you cannot possibly know that they are different. Some architectures represent the number one as 0x0001, others as 0x0100. And type systems are targeted at ***INSULATING*** users from such differences.

Author of SIRA_PRISE

The Forum for Discussion about The Third Manifesto and Related Matters

'Phantom type' for Attribute-Value pairs, in "popular languages" [was C# as a D]