The Forum for Discussion about The Third Manifesto and Related Matters

Please or Register to create posts and topics.

The type of <TCLOSE>

Musing on a couple of recent threads, especially types versus sets:

* Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.

What is the type of TCLOSE? Can that be expressed in the type-language of Tutorial D?

DTATRM Chapter 6, discussing RM Pre 19

Let r be a binary relation with attributes X and Y, both of the same type T. ...

TCLOSE needs to be applicable to any relation with two attributes, and at any type providing both attribs are at the same type. That seems to need parametric polymorphism for the attribute type, and poly-attribute-ism(?) for the attribute names. How to express that in the type system?

  • TCLOSE :: REL{ a t, b t } -> REL{ a t, b t } (?) in which:
  • :: says 'here comes the signature'.
  • Arrow blah1 -> blah2 means a function taking an operand of the first type, yielding a result of the second type.
  • t being lower case means it ranges over any type.
  • a, b being lower case means they range over any two (distinct) attribute names.

Now DTATRM/ TTM wants types to be sets. t we might take to 'stand for' some (scalar) type to be supplied. But are a, b types or components of types or what?

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

Quote from AntC on July 7, 2021, 7:27 am

Musing on a couple of recent threads, especially types versus sets:

* Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.

What is the type of TCLOSE? Can that be expressed in the type-language of Tutorial D?

TCLOSE is a function. In TTM/D and TD it is second class, not a value, does not have a type. In some other language/type system it might be a value of type function R=>R.

DTATRM Chapter 6, discussing RM Pre 19

Let r be a binary relation with attributes X and Y, both of the same type T. ...

TCLOSE needs to be applicable to any relation with two attributes, and at any type providing both attribs are at the same type. That seems to need parametric polymorphism for the attribute type, and poly-attribute-ism(?) for the attribute names. How to express that in the type system?

  • TCLOSE :: REL{ a t, b t } -> REL{ a t, b t } (?) in which:
  • :: says 'here comes the signature'.
  • Arrow blah1 -> blah2 means a function taking an operand of the first type, yielding a result of the second type.
  • t being lower case means it ranges over any type.
  • a, b being lower case means they range over any two (distinct) attribute names.

Now DTATRM/ TTM wants types to be sets. t we might take to 'stand for' some (scalar) type to be supplied. But are a, b types or components of types or what?

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

In TTM a type is a named set of values. As to the type of its argument and return value, some TTM/D might allow it to be so constrained but TD does not.

 

Andl - A New Database Language - andl.org
Quote from dandl on July 8, 2021, 1:08 am
Quote from AntC on July 7, 2021, 7:27 am

Musing on a couple of recent threads, especially types versus sets:

* Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.

What is the type of TCLOSE? Can that be expressed in the type-language of Tutorial D?

TCLOSE is a function. In TTM/D and TD it is second class, not a value, does not have a type. In some other language/type system it might be a value of type function R=>R.

DTATRM Chapter 6, discussing RM Pre 19

Let r be a binary relation with attributes X and Y, both of the same type T. ...

TCLOSE needs to be applicable to any relation with two attributes, and at any type providing both attribs are at the same type. That seems to need parametric polymorphism for the attribute type, and poly-attribute-ism(?) for the attribute names. How to express that in the type system?

  • TCLOSE :: REL{ a t, b t } -> REL{ a t, b t } (?) in which:
  • :: says 'here comes the signature'.
  • Arrow blah1 -> blah2 means a function taking an operand of the first type, yielding a result of the second type.
  • t being lower case means it ranges over any type.
  • a, b being lower case means they range over any two (distinct) attribute names.

Now DTATRM/ TTM wants types to be sets. t we might take to 'stand for' some (scalar) type to be supplied. But are a, b types or components of types or what?

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

In TTM a type is a named set of values. As to the type of its argument and return value, some TTM/D might allow it to be so constrained but TD does not.

 

Ok then a reduced question:

  • What's the type/how to describe it in Tutorial D's type language: for a relation eligible to be an operand to <TCLOSE>?
  • That is: exactly two attributes/degree two; both of the same type.
  • AFAICT the language of constraints encompasses eligible values of the given type, not eligible types/same-typeness; nor eligible degree-ness.

 

Quote from AntC on July 8, 2021, 7:35 am
Quote from dandl on July 8, 2021, 1:08 am
Quote from AntC on July 7, 2021, 7:27 am

Musing on a couple of recent threads, especially types versus sets:

* Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.

What is the type of TCLOSE? Can that be expressed in the type-language of Tutorial D?

TCLOSE is a function. In TTM/D and TD it is second class, not a value, does not have a type. In some other language/type system it might be a value of type function R=>R.

DTATRM Chapter 6, discussing RM Pre 19

Let r be a binary relation with attributes X and Y, both of the same type T. ...

TCLOSE needs to be applicable to any relation with two attributes, and at any type providing both attribs are at the same type. That seems to need parametric polymorphism for the attribute type, and poly-attribute-ism(?) for the attribute names. How to express that in the type system?

  • TCLOSE :: REL{ a t, b t } -> REL{ a t, b t } (?) in which:
  • :: says 'here comes the signature'.
  • Arrow blah1 -> blah2 means a function taking an operand of the first type, yielding a result of the second type.
  • t being lower case means it ranges over any type.
  • a, b being lower case means they range over any two (distinct) attribute names.

Now DTATRM/ TTM wants types to be sets. t we might take to 'stand for' some (scalar) type to be supplied. But are a, b types or components of types or what?

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

In TTM a type is a named set of values. As to the type of its argument and return value, some TTM/D might allow it to be so constrained but TD does not.

 

Ok then a reduced question:

  • What's the type/how to describe it in Tutorial D's type language: for a relation eligible to be an operand to <TCLOSE>?
  • That is: exactly two attributes/degree two; both of the same type.
  • AFAICT the language of constraints encompasses eligible values of the given type, not eligible types/same-typeness; nor eligible degree-ness.

As defined, Tutorial D doesn't have a means to specify an operator like TCLOSE in Tutorial D.  Indeed, it doesn't have a way to specify any of the usual relational operators, as there is no means to specify a generic relation, let alone constraints on headings.

Over the years, there has been discussion about ways to specify generic relations and other typesystem mechanics for handling user-defined relational operators including TCLOSE (two relations with two attributes, both of the same type), UNION (two relations with the same attributes), etc., but I don't recall any consensus on syntax/semantics, let alone anything that's made it into the official Tutorial D spec.

In Rel, all the requisite machinery exists (as it must) but isn't exposed as surface syntax.

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 AntC on July 8, 2021, 7:35 am
Quote from dandl on July 8, 2021, 1:08 am
Quote from AntC on July 7, 2021, 7:27 am

Musing on a couple of recent threads, especially types versus sets:

* Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.

What is the type of TCLOSE? Can that be expressed in the type-language of Tutorial D?

TCLOSE is a function. In TTM/D and TD it is second class, not a value, does not have a type. In some other language/type system it might be a value of type function R=>R.

DTATRM Chapter 6, discussing RM Pre 19

Let r be a binary relation with attributes X and Y, both of the same type T. ...

TCLOSE needs to be applicable to any relation with two attributes, and at any type providing both attribs are at the same type. That seems to need parametric polymorphism for the attribute type, and poly-attribute-ism(?) for the attribute names. How to express that in the type system?

  • TCLOSE :: REL{ a t, b t } -> REL{ a t, b t } (?) in which:
  • :: says 'here comes the signature'.
  • Arrow blah1 -> blah2 means a function taking an operand of the first type, yielding a result of the second type.
  • t being lower case means it ranges over any type.
  • a, b being lower case means they range over any two (distinct) attribute names.

Now DTATRM/ TTM wants types to be sets. t we might take to 'stand for' some (scalar) type to be supplied. But are a, b types or components of types or what?

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

In TTM a type is a named set of values. As to the type of its argument and return value, some TTM/D might allow it to be so constrained but TD does not.

 

Ok then a reduced question:

  • What's the type/how to describe it in Tutorial D's type language: for a relation eligible to be an operand to <TCLOSE>?
  • That is: exactly two attributes/degree two; both of the same type.
  • AFAICT the language of constraints encompasses eligible values of the given type, not eligible types/same-typeness; nor eligible degree-ness.

 

I rather thought that's where you were heading. So:

  • TCLOSE is a function with the signature T => T
  • T is required to be a generic relation of degree 2. The return value type is supplied by the compiler by type inference.
  • TTM proposes generic relational operators: RM VSS 6.
  • TTM does not prohibit (and therefore permits) a D that imposes a constraint on cardinatily for generic operators.
  • TD does not implement user defined generic relational operators.

As an aside, I have proposed that in TTM:

  • individual relation (and tuple) types be replaced by a single relation (and tuple) type (which of course would be generic)
  • headings be added as a type (syntactically a set of strings) for use as an argument to relational operators. Type inference is replaced by heading inference.

Given this proposal, it would be trivial to add a type constraint on cardinality.

Andl - A New Database Language - andl.org
Quote from dandl on July 9, 2021, 12:23 am
Quote from AntC on July 8, 2021, 7:35 am
Quote from dandl on July 8, 2021, 1:08 am
Quote from AntC on July 7, 2021, 7:27 am

Musing on a couple of recent threads, especially types versus sets:

* Types, on the other hand, are characterized by how elements of the type are built: we can construct elements of a type (and deconstruct them) in certain ways specific to the type.

What is the type of TCLOSE? Can that be expressed in the type-language of Tutorial D?

TCLOSE is a function. In TTM/D and TD it is second class, not a value, does not have a type. In some other language/type system it might be a value of type function R=>R.

DTATRM Chapter 6, discussing RM Pre 19

Let r be a binary relation with attributes X and Y, both of the same type T. ...

TCLOSE needs to be applicable to any relation with two attributes, and at any type providing both attribs are at the same type. That seems to need parametric polymorphism for the attribute type, and poly-attribute-ism(?) for the attribute names. How to express that in the type system?

  • TCLOSE :: REL{ a t, b t } -> REL{ a t, b t } (?) in which:
  • :: says 'here comes the signature'.
  • Arrow blah1 -> blah2 means a function taking an operand of the first type, yielding a result of the second type.
  • t being lower case means it ranges over any type.
  • a, b being lower case means they range over any two (distinct) attribute names.

Now DTATRM/ TTM wants types to be sets. t we might take to 'stand for' some (scalar) type to be supplied. But are a, b types or components of types or what?

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

In TTM a type is a named set of values. As to the type of its argument and return value, some TTM/D might allow it to be so constrained but TD does not.

 

Ok then a reduced question:

  • What's the type/how to describe it in Tutorial D's type language: for a relation eligible to be an operand to <TCLOSE>?
  • That is: exactly two attributes/degree two; both of the same type.
  • AFAICT the language of constraints encompasses eligible values of the given type, not eligible types/same-typeness; nor eligible degree-ness.

 

I rather thought that's where you were heading. So:

  • TCLOSE is a function with the signature T => T
  • T is required to be a generic relation of degree 2. The return value type is supplied by the compiler by type inference.
  • TTM proposes generic relational operators: RM VSS 6.
  • TTM does not prohibit (and therefore permits) a D that imposes a constraint on cardinatily for generic operators.

Please try to use terms correctly. Tutorial D already supports constraints on 'cardinality' -- that is, the number of tuples in a relation body. Here I'm talking about 'degree'.

  • TD does not implement user defined generic relational operators.

As an aside, I have proposed that in TTM:

  • individual relation (and tuple) types be replaced by a single relation (and tuple) type (which of course would be generic)

Yeah. That's dumber than removing tuples. "generic" in this case = unhelpfully vague. My tentative REL{ a t, b t} seems to fill the bill.

  • headings be added as a type (syntactically a set of strings) for use as an argument to relational operators. Type inference is replaced by heading inference.

Or ... Relation values consist of a Heading and a Body [RM Pre 10]. Type inference = heading inference, accessing the Heading component. We're already supplying the relation(s) as argument(s) to relational operators. If we passed the Headings separately, we'd need a mechanism to show which Heading belonged with which argument. Why double-up the number of arguments?

Given this proposal, it would be trivial to add a type constraint on cardinality.

cardinality degree. How would that differ to expressing the type constraint on the Heading component of a relation value?

You seem to have merely shuffled the deckchairs.

Please try to use terms correctly. Tutorial D already supports constraints on 'cardinality' -- that is, the number of tuples in a relation body. Here I'm talking about 'degree'.

Typo. Sorry. But you knew what I meant.

  • TD does not implement user defined generic relational operators.

As an aside, I have proposed that in TTM:

  • individual relation (and tuple) types be replaced by a single relation (and tuple) type (which of course would be generic)

Yeah. That's dumber than removing tuples. "generic" in this case = unhelpfully vague. My tentative REL{ a t, b t} seems to fill the bill.

It does not. And your dismissive response simply means you don't understand.

  • headings be added as a type (syntactically a set of strings) for use as an argument to relational operators. Type inference is replaced by heading inference.

Or ... Relation values consist of a Heading and a Body [RM Pre 10]. Type inference = heading inference, accessing the Heading component. We're already supplying the relation(s) as argument(s) to relational operators. If we passed the Headings separately, we'd need a mechanism to show which Heading belonged with which argument. Why double-up the number of arguments?

Rubbish.  The heading for a relation argument is determined by heading inference. A heading argument is needed for project, rename and extend, exactly as it is now in TD.

Given this proposal, it would be trivial to add a type constraint on cardinality.

cardinality degree. How would that differ to expressing the type constraint on the Heading component of a relation value?

You seem to have merely shuffled the deckchairs.

The problem it solved is with generics. It provides a single unified mechanism, rather than grafting on a whole new syntax.

Edit: And it is much friendlier to implement using existing GP languages. I have implemented it in C# and it should fit just as well into Java. A small addition to the language is required to perform heading inference, if it is not to be left to the runtime. A few languages have sufficiently powerful meta-programming for direct implementation. You can't do that with TTM.

BTW there is no need for a constraint on degree if the arguments for TCLOSE are (r1, r2, H<a,b>)where H is a heading argument of two attribute names.

Andl - A New Database Language - andl.org
Quote from AntC on July 7, 2021, 7:27 am

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

I'd say RELATION {attrNm AttributeName   attrType TypeName}   with relation values typically of cardinality 2 (but perhaps not necessarily always so, the usual suspect being a case in point)   can do whatever job you want to be done.

That could be the return type of an operator HEADING( ... ) which is ***obviously*** implemented one way or another in any system that parses relational expressions before evaluating them, but not necessarily exposed to the end-user in any language or sub-language of said system.

Quote from AntC on July 7, 2021, 7:27 am

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

If you find the idea of a single RELATION type "dumber" than TTM's notion of myriads of relation types, one for each possible heading, and you also want this discussion to make sense, there's no avoiding having to accept that there are also myriads of TCLOSE operators (one for each possible heading).

Why ?  Because an operator is a function, is a relation, is a subset of a cartesian product of domains.  Which domains ?  The relation type of the argument to the TCLOSE at hand.  So if H1 and H2 are distinct headings (both 'compatible' with the requirements imposed on them for their corresponding relation types being subjectible to TCLOSE), then REL{H1} and REL{H2} are distinct relation types, and then REL{H1} X REL{H1} and REL{H2} X REL{H2} are distinct cartesian products, and any subsets of the former is therefore necessarily distinct from any subset of the latter too.  So you arguably have TCLOSE{H1} and TCLOSE{H2} which are distinct operators.  Just TCLOSE can refer only to the entire collection/family/... of operators, and as such it does not make sense to try and pretend TCLOSE as such "has a type".

Let's say {H1} is {A BOOL   B BOOL}.  The tuple universe for that heading is size 4 : { {A true   B true}  {A true   B false}   {A false   B true}   {A false   B false} }.  Each of those 4 tuples can either or not appear in some relation value of that heading, leaving a relation universe of size 16 :  one relation of cardinality zero, one of card. 4, 4 of card. 1, 4 of card. 3, 6 of card. 2.  TCLOSE{H1} is then a set of 16 pairs of REL{H1} values.  Some of these pairs are :

( REL{H1} {} , REL{H1} {} )

( REL{H1} {TUP{A true   B true}} , REL{H1}{TUP{A true   B true}} )

( REL{H1} {TUP{A true   B false}   TUP{A false   B true}} , REL{H1}{TUP{A true   B true}   TUP{A false   B true}   TUP{A true   B true}   TUP{A true   B true}} )

Alternatively, you can apply the RM's technique of attribute naming to turn these ordered pairs into their unordered-but-named equivalent.  It does not materially affect the argument of how TCLOSE{H1} is a set.  Nor of how the codomain of TCLOSE{H1} (which in programming becomes the declared type of an invocation of that operator) is itself (by definition) a set (in this case the very relation type REL{H1} itself, or perhaps mathematically even more correct some proper subset of it) because otherwise we wouldn't have had a function(/operator) in the first place ...

Quote from Erwin on July 10, 2021, 3:04 pm
Quote from AntC on July 7, 2021, 7:27 am

I really can't see the type of TCLOSE as being a set; nor the type of its operand/result. "characterised by how elements of the type are built" seems more to the point.

If you find the idea of a single RELATION type "dumber" than TTM's notion of myriads of relation types, one for each possible heading, and you also want this discussion to make sense, there's no avoiding having to accept that there are also myriads of TCLOSE operators (one for each possible heading).

I can test Ints for equality; I can test Chars for equality; I can test Dates for equality; I can test Floats for equality; ... And that's just the scalars. Does that mean there are myriads of == operators? I can test TUP{ A Int }s for equality; I can test TUP{ A Char }s for equality; I can test TUP{ B Int }s for equality ... Does that mean there are myriads more == operators, one for each possible TUP heading? And myriads more more == operators, one for each REL{ ... } heading?

No: I say there is one == operator, overloaded for each (scalar) type; and structurally overloaded for each parametric type, like TUP{ A t }; and for each poly-attribute (as I said in my O.P.) TUP{ a t }.

Why ?  Because an operator is a function, is a relation, is a subset of a cartesian product of domains.

No. That's the set-based approach that doesn't even work for TTM Selectors/constructed types; let alone TUP, RELs.

  Which domains ?  The relation type of the argument to the TCLOSE at hand.  So if H1 and H2 are distinct headings (both 'compatible' with the requirements imposed on them for their corresponding relation types being subjectible to TCLOSE), then REL{H1} and REL{H2} are distinct relation types, and then REL{H1} X REL{H1} and REL{H2} X REL{H2} are distinct cartesian products, and any subsets of the former is therefore necessarily distinct from any subset of the latter too.  So you arguably have TCLOSE{H1} and TCLOSE{H2} which are distinct operators.  Just TCLOSE can refer only to the entire collection/family/... of operators, and as such it does not make sense to try and pretend TCLOSE as such "has a type".

Or ... You take a richer view of what a type is. Because the TTM set-based approach doesn't stretch. Then the type of an eligible operand to <TCLOSE> is REL{ a t, b t }.

Whereas if you say all RELs have the same type (with some hand-waving about generics); you can't then statically reject operands that are ill-typed for <TCLOSE> (except with more hand-waving).

Let's say {H1} is {A BOOL   B BOOL}.  The tuple universe for that heading is size 4 : { {A true   B true}  {A true   B false}   {A false   B true}   {A false   B false} }.  Each of those 4 tuples can either or not appear in some relation value of that heading, leaving a relation universe of size 16 :  one relation of cardinality zero, one of card. 4, 4 of card. 1, 4 of card. 3, 6 of card. 2.  TCLOSE{H1} is then a set of 16 pairs of REL{H1} values.  Some of these pairs are :

( REL{H1} {} , REL{H1} {} )

( REL{H1} {TUP{A true   B true}} , REL{H1}{TUP{A true   B true}} )

( REL{H1} {TUP{A true   B false}   TUP{A false   B true}} , REL{H1}{TUP{A true   B true}   TUP{A false   B true}   TUP{A true   B true}   TUP{A true   B true}} )

Alternatively, you can apply the RM's technique of attribute naming to turn these ordered pairs into their unordered-but-named equivalent.  It does not materially affect the argument of how TCLOSE{H1} is a set.  Nor of how the codomain of TCLOSE{H1} (which in programming becomes the declared type of an invocation of that operator) is itself (by definition) a set (in this case the very relation type REL{H1} itself, or perhaps mathematically even more correct some proper subset of it) because otherwise we wouldn't have had a function(/operator) in the first place ...