The Forum for Discussion about The Third Manifesto and Related Matters

Please or Register to create posts and topics.

Are inclusion dependencies reducible to foreign-key dependencies?

PreviousPage 6 of 9Next
Quote from Erwin on October 15, 2019, 6:50 am

Brian's issue is around the MST of an empty relation being OMEGA for all attributes, hence REL{A OMEGA, B OMEGA}.

The empty relation is a value of that type, so unlike OMEGA itself, types like REL {A OMEGA, B OMEGA} are not empty.

And per the rules as formulated an empty relation must be assignable to any variable whose type is a supertype of that empty relation's MST.  Meaning it must be assignable to, say, both a relvar of type {A PICTURE, B SOUND} as a relvar of type {A CHAR, B INT}.  (And this goes to show that the intersection type between these two relation types is not empty.)

These are plain facts, and it's not for you to choose whether you "buy that" or not.

No, these are never facts. They are your assertions, based on some kind of logic applied to proposals in a document (the IM). Facts are something quite different.

And Brian talked about alpha, not omega.

So yes, IM Pre 25 sets out maximal and minimal types for tuple and relation types, for any given set of attribute names. It does not say that values of those types should exist, and my expectation is that they would not, for consistency with scalars. Perhaps that was a D&D oversight?

Brian produced some pseudo-TD purporting to show a literal of these types, but nothing to say any compiler is required to implement them.

Now since the intersection type is not empty, it could possibly occur at run-time that an equality test between two such relvars would succeed.  And you could (as Brian seems to do) derive from that that an equality test must be accepted at compile time.

The alternative is to observe that the scenario can only occur with empty relations which means that 'R1 == R2' could also be written 'R1 == PHI && R2 == PHI' and then stick with the 'sensible' rule even if means a somewhat inelegant hackish exception.

In effect you are saying that (a) there are these weird relational values based on alpha or omega (b) they can be assigned to any relvar with matching attribute names regardless of type (c) therefore any two such relvars might be equal because they might both contain such a value.

I still don't buy it. No compiler writer will even raise a sweat dealing with this non-problem. Simplest way: there is no such value.

It has been discussed ad nauseam here (surprised ?) but I don't recall a firm conclusion coming out except "it's your D, you choose what you do".

Do you remember when? I have no recollection at all.

Andl - A New Database Language - andl.org
Quote from dandl on October 15, 2019, 11:48 pm
Quote from Erwin on October 15, 2019, 6:50 am

Brian's issue is around the MST of an empty relation being OMEGA for all attributes, hence REL{A OMEGA, B OMEGA}.

The empty relation is a value of that type, so unlike OMEGA itself, types like REL {A OMEGA, B OMEGA} are not empty.

And per the rules as formulated an empty relation must be assignable to any variable whose type is a supertype of that empty relation's MST.  Meaning it must be assignable to, say, both a relvar of type {A PICTURE, B SOUND} as a relvar of type {A CHAR, B INT}.  (And this goes to show that the intersection type between these two relation types is not empty.)

These are plain facts, and it's not for you to choose whether you "buy that" or not.

No, these are never facts. They are your assertions, based on some kind of logic applied to proposals in a document (the IM). Facts are something quite different.

And Brian talked about alpha, not omega.

So yes, IM Pre 25 sets out maximal and minimal types for tuple and relation types, for any given set of attribute names. It does not say that values of those types should exist, and my expectation is that they would not, for consistency with scalars. Perhaps that was a D&D oversight?

Brian produced some pseudo-TD purporting to show a literal of these types, but nothing to say any compiler is required to implement them.

Now since the intersection type is not empty, it could possibly occur at run-time that an equality test between two such relvars would succeed.  And you could (as Brian seems to do) derive from that that an equality test must be accepted at compile time.

The alternative is to observe that the scenario can only occur with empty relations which means that 'R1 == R2' could also be written 'R1 == PHI && R2 == PHI' and then stick with the 'sensible' rule even if means a somewhat inelegant hackish exception.

In effect you are saying that (a) there are these weird relational values based on alpha or omega (b) they can be assigned to any relvar with matching attribute names regardless of type (c) therefore any two such relvars might be equal because they might both contain such a value.

I still don't buy it. No compiler writer will even raise a sweat dealing with this non-problem. Simplest way: there is no such value.

It has been discussed ad nauseam here (surprised ?) but I don't recall a firm conclusion coming out except "it's your D, you choose what you do".

Do you remember when? I have no recollection at all.

Here's the logic : a relation value's MST is a given relation type iff :

(1) FORALL tuples in the given relation value, the tuple is heading-compatible with the [heading corresponding to] the given relation type, and

(2) There is no proper subtype of the given relation type for which (1) holds

Given that the empty relation is empty (i.e. has no tuples), (1) degenerates to true and (2) then comes to mean that the MST will be that in which all attribute type declarations are themselves the minimal type i.e. :

  • all scalar type declarations are type OMEGA
  • all nonscalar type declarations are the minimal type declaration corresponding to the nonscalar type concerned

The "weird value" you are talking about is just the empty relation of any relation type (/heading), and no, the "consistency with scalars" you "expect" (I did too at the time, FWIW, and probably many others besides me) just isn't there.  Whether to call that an "oversight" or not, I wouldn't know.

(It might be possible to deliberately re-introduce the "consistency with scalars" by creating ("for the mere sake of it") an empty type (or even one for each possible heading) REL_OMEGA which is a subtype of those nonempty minimal relation types that currently contain only the empty relation of their corresponding heading.  Such possibility has not been investigated in detail AFAICT and it on the face of it it looks like it won't fix Brian's issue.)

But plain decreeing "there is no such value" is just plain denying the light of day.

 

Author of SIRA_PRISE
Quote from Erwin on October 16, 2019, 6:46 am

Here's the logic : a relation value's MST is a given relation type iff :

(1) FORALL tuples in the given relation value, the tuple is heading-compatible with the [heading corresponding to] the given relation type, and

(2) There is no proper subtype of the given relation type for which (1) holds

Given that the empty relation is empty (i.e. has no tuples), (1) degenerates to true and (2) then comes to mean that the MST will be that in which all attribute type declarations are themselves the minimal type i.e. :

  • all scalar type declarations are type OMEGA
  • all nonscalar type declarations are the minimal type declaration corresponding to the nonscalar type concerned

The "weird value" you are talking about is just the empty relation of any relation type (/heading), and no, the "consistency with scalars" you "expect" (I did too at the time, FWIW, and probably many others besides me) just isn't there.  Whether to call that an "oversight" or not, I wouldn't know.

(It might be possible to deliberately re-introduce the "consistency with scalars" by creating ("for the mere sake of it") an empty type (or even one for each possible heading) REL_OMEGA which is a subtype of those nonempty minimal relation types that currently contain only the empty relation of their corresponding heading.  Such possibility has not been investigated in detail AFAICT and it on the face of it it looks like it won't fix Brian's issue.)

But plain decreeing "there is no such value" is just plain denying the light of day.

OK, now that's beginning to make sense. We can forget about Brian's reference to a specific literal form REL { X ALPHA, Y ALPHA }{}, that's not what you're arguing at all.

You're saying that if the IM is in force, every empty relation of type T is not only a value of type T, it's also a value of type T_omega, which is the minimal type with respect to type T (per IM Pre 25). Actually the one and only value, because there are no values of type omega so all possible tuple values are excluded (IM Pre 20a).

So in TD speak, the value REL { X int, Y char } {} is a value both of type REL{ X int, Y char } and of type REL{ X omega, Y omega }, and for this reason all empty values with a given set of attribute names are the same value, so they're equal.

I'm still short of buying this conclusion. It obviously has no effect on the comparison of non-empty relational values; it serves only to make every empty relation of type T1 equal to any other empty relation of type T2 if T1 and T2 have the same attribute names. After a single step of renaming, any two empty relations of whatever types are equal if they have the same degree. These are plainly counter-intuitive consequences. It has the same character as a using a divide-by-zero to prove that pi is integral.

I would be curious to know whether D&D noticed this issue and/or what they thought or think might be done about. It looks like an oversight, something that should be clarified and/or corrected.

 

Andl - A New Database Language - andl.org
Quote from dandl on October 16, 2019, 1:34 pm
Quote from Erwin on October 16, 2019, 6:46 am

Here's the logic : a relation value's MST is a given relation type iff :

(1) FORALL tuples in the given relation value, the tuple is heading-compatible with the [heading corresponding to] the given relation type, and

(2) There is no proper subtype of the given relation type for which (1) holds

Given that the empty relation is empty (i.e. has no tuples), (1) degenerates to true and (2) then comes to mean that the MST will be that in which all attribute type declarations are themselves the minimal type i.e. :

  • all scalar type declarations are type OMEGA
  • all nonscalar type declarations are the minimal type declaration corresponding to the nonscalar type concerned

The "weird value" you are talking about is just the empty relation of any relation type (/heading), and no, the "consistency with scalars" you "expect" (I did too at the time, FWIW, and probably many others besides me) just isn't there.  Whether to call that an "oversight" or not, I wouldn't know.

(It might be possible to deliberately re-introduce the "consistency with scalars" by creating ("for the mere sake of it") an empty type (or even one for each possible heading) REL_OMEGA which is a subtype of those nonempty minimal relation types that currently contain only the empty relation of their corresponding heading.  Such possibility has not been investigated in detail AFAICT and it on the face of it it looks like it won't fix Brian's issue.)

But plain decreeing "there is no such value" is just plain denying the light of day.

OK, now that's beginning to make sense. We can forget about Brian's reference to a specific literal form REL { X ALPHA, Y ALPHA }{}, that's not what you're arguing at all.

You're saying that if the IM is in force, every empty relation of type T is not only a value of type T, it's also a value of type T_omega, which is the minimal type with respect to type T (per IM Pre 25). Actually the one and only value, because there are no values of type omega so all possible tuple values are excluded (IM Pre 20a).

So in TD speak, the value REL { X int, Y char } {} is a value both of type REL{ X int, Y char } and of type REL{ X omega, Y omega }, and for this reason all empty values with a given set of attribute names are the same value, so they're equal.

I'm still short of buying this conclusion. It obviously has no effect on the comparison of non-empty relational values; it serves only to make every empty relation of type T1 equal to any other empty relation of type T2 if T1 and T2 have the same attribute names. After a single step of renaming, any two empty relations of whatever types are equal if they have the same degree. These are plainly counter-intuitive consequences. It has the same character as a using a divide-by-zero to prove that pi is integral.

I would be curious to know whether D&D noticed this issue and/or what they thought or think might be done about. It looks like an oversight, something that should be clarified and/or corrected.

If I recall correctly (and might check later, as time permits), it is discussed in at least Date's Type Inheritance and Relational Theory, which expands on the Part III Type Inheritance section of Database Explorations.

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
Quote from Dave Voorhis on October 16, 2019, 1:46 pm
Quote from dandl on October 16, 2019, 1:34 pm
Quote from Erwin on October 16, 2019, 6:46 am

Here's the logic : a relation value's MST is a given relation type iff :

(1) FORALL tuples in the given relation value, the tuple is heading-compatible with the [heading corresponding to] the given relation type, and

(2) There is no proper subtype of the given relation type for which (1) holds

Given that the empty relation is empty (i.e. has no tuples), (1) degenerates to true and (2) then comes to mean that the MST will be that in which all attribute type declarations are themselves the minimal type i.e. :

  • all scalar type declarations are type OMEGA
  • all nonscalar type declarations are the minimal type declaration corresponding to the nonscalar type concerned

The "weird value" you are talking about is just the empty relation of any relation type (/heading), and no, the "consistency with scalars" you "expect" (I did too at the time, FWIW, and probably many others besides me) just isn't there.  Whether to call that an "oversight" or not, I wouldn't know.

(It might be possible to deliberately re-introduce the "consistency with scalars" by creating ("for the mere sake of it") an empty type (or even one for each possible heading) REL_OMEGA which is a subtype of those nonempty minimal relation types that currently contain only the empty relation of their corresponding heading.  Such possibility has not been investigated in detail AFAICT and it on the face of it it looks like it won't fix Brian's issue.)

But plain decreeing "there is no such value" is just plain denying the light of day.

OK, now that's beginning to make sense. We can forget about Brian's reference to a specific literal form REL { X ALPHA, Y ALPHA }{}, that's not what you're arguing at all.

You're saying that if the IM is in force, every empty relation of type T is not only a value of type T, it's also a value of type T_omega, which is the minimal type with respect to type T (per IM Pre 25). Actually the one and only value, because there are no values of type omega so all possible tuple values are excluded (IM Pre 20a).

So in TD speak, the value REL { X int, Y char } {} is a value both of type REL{ X int, Y char } and of type REL{ X omega, Y omega }, and for this reason all empty values with a given set of attribute names are the same value, so they're equal.

I'm still short of buying this conclusion. It obviously has no effect on the comparison of non-empty relational values; it serves only to make every empty relation of type T1 equal to any other empty relation of type T2 if T1 and T2 have the same attribute names. After a single step of renaming, any two empty relations of whatever types are equal if they have the same degree. These are plainly counter-intuitive consequences. It has the same character as a using a divide-by-zero to prove that pi is integral.

I would be curious to know whether D&D noticed this issue and/or what they thought or think might be done about. It looks like an oversight, something that should be clarified and/or corrected.

If I recall correctly (and might check later, as time permits), it is discussed in at least Date's Type Inheritance and Relational Theory, which expands on the Part III Type Inheritance section of Database Explorations.

Now that I'm at it, I even wonder if relational minimal types are always guaranteed to be singleton.

Take a relation type with only RVA's, say REL {RVA REL {I INT}}.

As already observed, the empty relation of that type is member of the minimal type REL {RVA REL{I OMEGA}}.  But what about REL {TUP {RVA REL {I INT}{}}} ?

REL {RVA REL{I OMEGA}} is itself minimal which guarantees (2) in my original explanation,

and the MST of REL {I INT}{} is REL {I OMEGA} which clearly makes this value heading-compatible too, so (1) is satisfied too.

It seems. :-o

Author of SIRA_PRISE
Quote from Dave Voorhis on October 16, 2019, 1:46 pm

OK, now that's beginning to make sense. We can forget about Brian's reference to a specific literal form REL { X ALPHA, Y ALPHA }{}, that's not what you're arguing at all.

You're saying that if the IM is in force, every empty relation of type T is not only a value of type T, it's also a value of type T_omega, which is the minimal type with respect to type T (per IM Pre 25). Actually the one and only value, because there are no values of type omega so all possible tuple values are excluded (IM Pre 20a).

So in TD speak, the value REL { X int, Y char } {} is a value both of type REL{ X int, Y char } and of type REL{ X omega, Y omega }, and for this reason all empty values with a given set of attribute names are the same value, so they're equal.

I'm still short of buying this conclusion. It obviously has no effect on the comparison of non-empty relational values; it serves only to make every empty relation of type T1 equal to any other empty relation of type T2 if T1 and T2 have the same attribute names. After a single step of renaming, any two empty relations of whatever types are equal if they have the same degree. These are plainly counter-intuitive consequences. It has the same character as a using a divide-by-zero to prove that pi is integral.

I would be curious to know whether D&D noticed this issue and/or what they thought or think might be done about. It looks like an oversight, something that should be clarified and/or corrected.

If I recall correctly (and might check later, as time permits), it is discussed in at least Date's Type Inheritance and Relational Theory, which expands on the Part III Type Inheritance section of Database Explorations.

I don't think I'd ever heard of it, and certainly never read it. I found a free copy on line, but I'm not sure where to look for answers. I didn't easily find anything useful Perhaps you know where to look.

I gave some more thought to this overnight. I think the IM is trying to set out a kind of hierarchy around a type T (scalar or not):

maxT > rootT >= supT >= T >= subT >= leafT > minT

Max and min are defined with reference to alpha and omega. They are simply markers for the boundaries of the type system. Root/leaf types are defined as the furthest you can go following super/sub types within the bounds set by max/min. Those type markers play no role in creating (selecting) values, or in comparing values. Values are compared based on their position within a type hierarchy, which is based on a single rootT.

The IM says that there are no scalar values of type alpha or omega. As a result, it is not possible to create (select) a tuple or relation value with an explicit mention of a value of type alpha or omega. Brian was wrong to do that.

The logical path presented by Erwin purports to introduce such a value implicitly, as a degenerate case when a relation is empty. I say that each empty relation still belongs to a specific type hierarchy and has a type that does not mention omega, and that such values are compared for equality by virtue of their positions in their respective type hierarchies and not by any shared minimal type.

In other words, REL{X T1,Y T2}{} and REL{X T3,Y T4}{} have the same minimal type with reference to T, which in each case is REL{X omega,Y omega} but they are of different types and are (or may be) different values because of how comparison of values works.

 

 

 

 

Andl - A New Database Language - andl.org
Quote from dandl on October 17, 2019, 12:41 am
Quote from Dave Voorhis on October 16, 2019, 1:46 pm

OK, now that's beginning to make sense. We can forget about Brian's reference to a specific literal form REL { X ALPHA, Y ALPHA }{}, that's not what you're arguing at all.

You're saying that if the IM is in force, every empty relation of type T is not only a value of type T, it's also a value of type T_omega, which is the minimal type with respect to type T (per IM Pre 25). Actually the one and only value, because there are no values of type omega so all possible tuple values are excluded (IM Pre 20a).

So in TD speak, the value REL { X int, Y char } {} is a value both of type REL{ X int, Y char } and of type REL{ X omega, Y omega }, and for this reason all empty values with a given set of attribute names are the same value, so they're equal.

I'm still short of buying this conclusion. It obviously has no effect on the comparison of non-empty relational values; it serves only to make every empty relation of type T1 equal to any other empty relation of type T2 if T1 and T2 have the same attribute names. After a single step of renaming, any two empty relations of whatever types are equal if they have the same degree. These are plainly counter-intuitive consequences. It has the same character as a using a divide-by-zero to prove that pi is integral.

I would be curious to know whether D&D noticed this issue and/or what they thought or think might be done about. It looks like an oversight, something that should be clarified and/or corrected.

If I recall correctly (and might check later, as time permits), it is discussed in at least Date's Type Inheritance and Relational Theory, which expands on the Part III Type Inheritance section of Database Explorations.

I don't think I'd ever heard of it, and certainly never read it. I found a free copy on line, but I'm not sure where to look for answers. I didn't easily find anything useful Perhaps you know where to look.

I gave some more thought to this overnight. I think the IM is trying to set out a kind of hierarchy around a type T (scalar or not):

maxT > rootT >= supT >= T >= subT >= leafT > minT

Max and min are defined with reference to alpha and omega. They are simply markers for the boundaries of the type system. Root/leaf types are defined as the furthest you can go following super/sub types within the bounds set by max/min. Those type markers play no role in creating (selecting) values, or in comparing values. Values are compared based on their position within a type hierarchy, which is based on a single rootT.

I'm no expert on the IM. But perhaps that means I can help out here. The IM is a nominative (or nominal) type system: so yes the position of a named type within the hierarchy is defined relative to other named types. But also the IM is based on types-as-sets of values and Specialisation-by-constraint: If T >= subT that must be because the declared constraint for named type subT can be inferred to be more restrictive than the constraint declared on T. (And T is more constrained than rootT, by assumption.) Given distinct T >= subT1, T >= subT2, we can infer there must be an intersection of subT1, subT2's constraints. That intersection might be empty, or might be some set of values for which there's no nominal type declared. If it's provably empty, it must be omega (which is a named type).

That leads to the (for me) bizarre situation that omega is a subtype of rootT, rootS, rootR, ... that is, every scalar type. Bizarre because the whole point of a type system is to keep sets-of-values apart. I'm familiar with nominative type systems that include named types that contain no values. They're very useful for certain sorts of type-safe type-level programming. It would be a horror if those all got collapsed into the same type.

The IM says that there are no scalar values of type alpha or omega. As a result, it is not possible to create (select) a tuple or relation value with an explicit mention of a value of type alpha or omega. Brian was wrong to do that.

Well if I have an empty relation of degree 1, what is the MST of its attribute? I want to say that for each rootT there is an omegaT which is 'the' subtype of T that contains no values, in which T is the declared (or inferred) attribute type.

In that case, I'd suspect we have no need for omega. That is, types form a hierarchy (or semilattice with alpha at the top) not a lattice. In that case, I question whether we need alpha, especially since there can be no scalar types at alpha.

The logical path presented by Erwin purports to introduce such a value implicitly, as a degenerate case when a relation is empty. I say that each empty relation still belongs to a specific type hierarchy and has a type that does not mention omega, and that such values are compared for equality by virtue of their positions in their respective type hierarchies and not by any shared minimal type.

In other words, REL{X T1,Y T2}{} and REL{X T3,Y T4}{} have the same minimal type with reference to T, which in each case is REL{X omega,Y omega} but they are of different types and are (or may be) different values because of how comparison of values works.

 

 

 

 

 

Quote from AntC on October 17, 2019, 1:52 am

I'm no expert on the IM. But perhaps that means I can help out here.

Gracious of you.

Well if I have an empty relation of degree 1, what is the MST of its attribute? I want to say that for each rootT there is an omegaT which is 'the' subtype of T that contains no values, in which T is the declared (or inferred) attribute type.

In that case, I'd suspect we have no need for omega. That is, types form a hierarchy (or semilattice with alpha at the top) not a lattice. In that case, I question whether we need alpha, especially since there can be no scalar types at alpha.

Both alpha and omega are notional types used to mark the top and bottom of a type graph (which may or may not be a 'lattice' -- see Type-Inheritance-and-Relational-Theory), without actually having any need to really exist. The MST/LST are the types you get when you trace the graph as far as you can, to the point where the next type would be omega/alpha. So a root type is just below alpha and a leaf type is just above omega. Every value V of declared type T is also a value of:

  • its MST (which I think is always some leafT, but that's not explicitly stated)
  • its rootT
  • the super-types of its MST that lead to the rootT

One might think that V is also a value of :

  • its maximal type (alpha or T_alpha)
  • its minimal type (omega or T_omega).

But values are only ever created (selected), assigned, compared or used in expressions on the basis of one of the first three type categories, never those two.

In answer to your questions:

  1. The attribute is part of its type signature, but the MST is a property of a value and the attribute has none. But the empty relation is a value and then it's a valid question. I expect that using the declared type as the MST would produce the right result, but I haven't worked through the detail.
  2. The need for alpha and omega is only as 'out of bounds' markers, not as real usable types.
Andl - A New Database Language - andl.org
Quote from AntC on October 17, 2019, 1:52 am

Well if I have an empty relation of degree 1, what is the MST of its attribute? I want to say that for each rootT there is an omegaT which is 'the' subtype of T that contains no values, in which T is the declared (or inferred) attribute type.

In that case, I'd suspect we have no need for omega. That is, types form a hierarchy (or semilattice with alpha at the top) not a lattice. In that case, I question whether we need alpha, especially since there can be no scalar types at alpha.

 

"What is the MST of its attribute" is a wrong question to ask.  MST is a property of a value, not of an attribute of a nonscalar value (an attribute is a member of a heading / nonscalar type declaration, but an attribute is not a value).  So while you can ask what the MST is of an empty relation of some relation type, and it would be answerable, your question isn't really answerable.  The MST of your empty relation will have an attribute declared to be of type the minimal type corresponding to the attribute type declaration in the relation type your empty relation is declared to be of (OMEGA if that attribute is scalar).

Having OMEGA on the scalars is a prerequisite, or at least very hard to avoid, for doing nonscalar inheritance the way TTM (/its authors) wants to do it.

Your alternative creates "difficulties" once you start creating union types.  You must see to it that you also create "the" corresponding empty type of that union type, and how it relates to "the" empty types corresponding to the participants in the union.  You're going to have lots and lots of empty types at the bottom of your type lattice.

The TTM IM was built on the (alas unenforceable) assumption that the type system IS a lattice (well three lattices if my understanding of lattices is correct -scalars, tuples, relations-), which guarantees a unique MST for every value in the system (which, e.g., facilitates handling literals as an expression of declared type that MST).

 

Author of SIRA_PRISE
Quote from dandl on October 17, 2019, 11:52 pm
Quote from AntC on October 17, 2019, 1:52 am

 

Well if I have an empty relation of degree 1, what is the MST of its attribute? I want to say that for each rootT there is an omegaT which is 'the' subtype of T that contains no values, in which T is the declared (or inferred) attribute type.

In that case, I'd suspect we have no need for omega. That is, types form a hierarchy (or semilattice with alpha at the top) not a lattice. In that case, I question whether we need alpha, especially since there can be no scalar types at alpha.

 

In answer to your questions:

  1. The attribute is part of its type signature, but the MST is a property of a value and the attribute has none. But the empty relation is a value and then it's a valid question. I expect that using the declared type as the MST would produce the right result, but I haven't worked through the detail.
  2. The need for alpha and omega is only as 'out of bounds' markers, not as real usable types.

I think the sticking point is Rm Pre 1 (no less):

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

The "and therefore" at the end is just wrong in case either of S1, S2 are empty: their intersection is empty, therefore they're disjoint. If both are empty, they're disjoint and equal sets.

And/or the author of RM Pre 1 doesn't understand nominative typing: if two types have distinct names, they're not the same type, irrespective of whether those names denote the same set of values. Specifically we've got empty sets of values at omegaT1, omegaT2 or leafT1, leafT2 whatever we're calling them.

RM Pre 1 goes on to a rather wooly exclusion "... with the exception of the system-defined type omega ...", but that's talking about the definition of a type, not its set of values.

PreviousPage 6 of 9Next