First and second class citizens in TTM

#51 · June 23, 2019, 4:10 pm

Quote from AntC on June 23, 2019, 4:10 pm

Quote from Hugh on June 23, 2019, 1:24 pm

Quote from AntC on June 23, 2019, 12:59 am

Quote from Hugh on June 22, 2019, 4:20 pm

Quote from AntC on June 22, 2019, 6:23 am

Quote from Hugh on June 11, 2019, 2:57 pm

Quote from AntC on June 11, 2019, 2:05 pm

Quote from Hugh on June 11, 2019, 10:40 am

Our reason for mandating BOOLEAN was to correct what we retrospectively regarded as an omission by Codd, ...

Mandating BOOLEAN is indeed sensible in practice; but in theory ...

RM Pre 1 for BOOLEAN prescribes "D shall support all four monadic and 16 dyadic logical operators, directly or indirectly, for this type." Then we could mimic Boolean operators using DUM, DEE as the values and traditional relational operators for all the logic you might need.

TTM prescribes BOOLEAN types to describe the results of evaluating integrity constraints (RM Pre 23). Typical practice (in Tutorial D) is that the formula for an integrity constraint is of the form IS_EMPTY( ... ).

We'd want DEE to correspond to TRUE, so the equivalent of IS_EMPTY( ... ) in constraints would be DEE NOT MATCHING ( ... ).

It's not very clear (IIRC from Chris's analysis of Codd's early papers) whether Codd omitted degree zero relations; or whether he anticipated them but suppressed that thought because it would cause conniptions amongst IBM engineers and top brass(?)

But DEE and DUM (which Codd also omitted and in fact deprecated, asking, "What are they for?") aren't truth values.

There's that slippery verb ' to be' again. I think you're failing to distinguish abstrep (a logical/abstract truth value) vs possrep (its representation in some D).

I think I can reasonably claim to understand that distinction quite well. A possrep is a syntactical device to define several necessary operators in one fell swoop. Antc's comment seems to be suggesting that 0-adic relations be used as possrep components for type BOOLEAN. All right then, the user-defined scalar type definition would look like this:

TYPE BOOLEAN POSSREP {DEEDUM RELATION{}};

No, there's no need to define a distinct type to represent BOOLEAN. You could use "BOOLEAN" as a typename alias (that Tutorial D does not have, see other discussions) to denote values of type RELATION constrained to degree zero.

And if BOOLEAN is not system-defined, users would be required under TTM to give such a definition.

But TTM also requires support for truth-valued equality comparisons, so "=" would have to be user-defined too.

You're repeating the point from an earlier message, and that I rather think I answered comprehensively. If everything is a relation (and the the possrep for scalar values is a relation of cardinality one degree one), then you already have scalar equality comparison: it's spelled JOIN (result projected on to degree zero).

And it has to be available for value-pairs of every type. I'm prepared to be convinced that a generic signature might be possible, but what about the implementation. How can I write a RETURN statement that returns BOOLEAN(TABLE_DEE) if the operands are the selfsame value, otherwise BOOLEAN(TABLE_DUM)?

I note in passing that TRUE and FALSE could be user-defined operators: OPERATOR TRUE ( ) RETURNS BOOLEAN; RETURN BOOLEAN(TABLE_DEE); END OPERATOR, and likewise FALSE(), and the language might permit parens to be omitted in niladic operator invocations.

TRUE, FALSE could be aliases for values DEE, DUM. Not operators, not variables: what some languages call "manifest constants".

But you appear now to be treating DEE and DUM as replacements for TRUE and FALSE, so what was all that about possreps for?

DEE, DUM (or their aliases TRUE, FALSE) are possreps in some D for the abstrep truth values.

As for your "explanation" about "=", please show me how to write an expression to replace "1 = 2" using JOIN.

But, but! That's moving the goalposts. Up to now you've been talking about = as comparison (RM Pre 8). Replace 1 = 2 is some sort of update, I'd rather spell that 1 := 2. You presumably mean in full something like UPDATE r SET x := 2 WHERE x = 1; (apologies for the SQL). As I said, we assume an unlimited supply of relcons (same style as Appendix A PLUS). For this exercise all I need is a couple of one-tuple relcons:
WITH There := REL{TUP{x 1, x' 2}}, Back := REL{TUP{x 2, x' 2}} :
r := ((r COMPOSE There) COMPOSE Back) InnerUnion (r NOT MATCHING There);
// in which
x COMPOSE y =df (x JOIN y) REMOVE (x InnerUnion y)
REMOVE =df the solution to forall x y [(x REMOVE (x REMOVE y)) = x InnerUnion (y JOIN DUM)]
NOT MATCHING =df the solution to forall x y [(x NOT MATCHING y) JOIN (x JOIN y) = (x JOIN y) JOIN DUM
                                             & (x NOT MATCHING y) InnerUnion (x JOIN y) = x]
InnerUnion =df the solution to forall x y z [ (x = (x JOIN z) & y = (y JOIN z))
                                              <-> (x InnerUnion y) = ((x InnerUnion y) JOIN z)]
You'll note all those definitions are ultimately in terms of JOIN (plus the usual machinery of FOL over the domain of relation values). Actually DUM can be defined as the solution to an expression in terms of JOIN/it's not a primitive; and of course DEE is merely the identity for JOIN.

You could perhaps using DUM to represent zero, then REL{I REL{}}{I REL{}} to represent 1, and so on for the remaining natural numbers, but what about comparison of values of other types?

It wasn't a serious suggestion for relations all the way down even into scalar types. I'll stick with the 'supremely unconcerned'/types are orthogonal to model.

Quote from Hugh on June 23, 2019, 1:24 pm

Quote from AntC on June 23, 2019, 12:59 am

Quote from Hugh on June 22, 2019, 4:20 pm

Quote from AntC on June 22, 2019, 6:23 am

Quote from Hugh on June 11, 2019, 2:57 pm

Quote from AntC on June 11, 2019, 2:05 pm

Quote from Hugh on June 11, 2019, 10:40 am

Our reason for mandating BOOLEAN was to correct what we retrospectively regarded as an omission by Codd, ...

Mandating BOOLEAN is indeed sensible in practice; but in theory ...

RM Pre 1 for BOOLEAN prescribes "D shall support all four monadic and 16 dyadic logical operators, directly or indirectly, for this type." Then we could mimic Boolean operators using DUM, DEE as the values and traditional relational operators for all the logic you might need.

TTM prescribes BOOLEAN types to describe the results of evaluating integrity constraints (RM Pre 23). Typical practice (in Tutorial D) is that the formula for an integrity constraint is of the form IS_EMPTY( ... ).

We'd want DEE to correspond to TRUE, so the equivalent of IS_EMPTY( ... ) in constraints would be DEE NOT MATCHING ( ... ).

It's not very clear (IIRC from Chris's analysis of Codd's early papers) whether Codd omitted degree zero relations; or whether he anticipated them but suppressed that thought because it would cause conniptions amongst IBM engineers and top brass(?)

But DEE and DUM (which Codd also omitted and in fact deprecated, asking, "What are they for?") aren't truth values.

There's that slippery verb ' to be' again. I think you're failing to distinguish abstrep (a logical/abstract truth value) vs possrep (its representation in some D).

I think I can reasonably claim to understand that distinction quite well. A possrep is a syntactical device to define several necessary operators in one fell swoop. Antc's comment seems to be suggesting that 0-adic relations be used as possrep components for type BOOLEAN. All right then, the user-defined scalar type definition would look like this:

TYPE BOOLEAN POSSREP {DEEDUM RELATION{}};

No, there's no need to define a distinct type to represent BOOLEAN. You could use "BOOLEAN" as a typename alias (that Tutorial D does not have, see other discussions) to denote values of type RELATION constrained to degree zero.

And if BOOLEAN is not system-defined, users would be required under TTM to give such a definition.

But TTM also requires support for truth-valued equality comparisons, so "=" would have to be user-defined too.

You're repeating the point from an earlier message, and that I rather think I answered comprehensively. If everything is a relation (and the the possrep for scalar values is a relation of cardinality one degree one), then you already have scalar equality comparison: it's spelled JOIN (result projected on to degree zero).

And it has to be available for value-pairs of every type. I'm prepared to be convinced that a generic signature might be possible, but what about the implementation. How can I write a RETURN statement that returns BOOLEAN(TABLE_DEE) if the operands are the selfsame value, otherwise BOOLEAN(TABLE_DUM)?

I note in passing that TRUE and FALSE could be user-defined operators: OPERATOR TRUE ( ) RETURNS BOOLEAN; RETURN BOOLEAN(TABLE_DEE); END OPERATOR, and likewise FALSE(), and the language might permit parens to be omitted in niladic operator invocations.

TRUE, FALSE could be aliases for values DEE, DUM. Not operators, not variables: what some languages call "manifest constants".

But you appear now to be treating DEE and DUM as replacements for TRUE and FALSE, so what was all that about possreps for?

DEE, DUM (or their aliases TRUE, FALSE) are possreps in some D for the abstrep truth values.

As for your "explanation" about "=", please show me how to write an expression to replace "1 = 2" using JOIN.

But, but! That's moving the goalposts. Up to now you've been talking about = as comparison (RM Pre 8). Replace 1 = 2 is some sort of update, I'd rather spell that 1 := 2. You presumably mean in full something like UPDATE r SET x := 2 WHERE x = 1; (apologies for the SQL). As I said, we assume an unlimited supply of relcons (same style as Appendix A PLUS). For this exercise all I need is a couple of one-tuple relcons:

WITH There := REL{TUP{x 1, x' 2}}, Back := REL{TUP{x 2, x' 2}} :
r := ((r COMPOSE There) COMPOSE Back) InnerUnion (r NOT MATCHING There);
// in which
x COMPOSE y =df (x JOIN y) REMOVE (x InnerUnion y)
REMOVE =df the solution to forall x y [(x REMOVE (x REMOVE y)) = x InnerUnion (y JOIN DUM)]
NOT MATCHING =df the solution to forall x y [(x NOT MATCHING y) JOIN (x JOIN y) = (x JOIN y) JOIN DUM
                                             & (x NOT MATCHING y) InnerUnion (x JOIN y) = x]
InnerUnion =df the solution to forall x y z [ (x = (x JOIN z) & y = (y JOIN z))
                                              <-> (x InnerUnion y) = ((x InnerUnion y) JOIN z)]

You'll note all those definitions are ultimately in terms of JOIN (plus the usual machinery of FOL over the domain of relation values). Actually DUM can be defined as the solution to an expression in terms of JOIN/it's not a primitive; and of course DEE is merely the identity for JOIN.

You could perhaps using DUM to represent zero, then REL{I REL{}}{I REL{}} to represent 1, and so on for the remaining natural numbers, but what about comparison of values of other types?

It wasn't a serious suggestion for relations all the way down even into scalar types. I'll stick with the 'supremely unconcerned'/types are orthogonal to model.

#52 · June 24, 2019, 1:34 pm

It never occurred to me that somebody might interpret my use of "replace" the way Antc has.

With support for scalar type INTEGER I can write "1 = 2" to express comparison for equality on those two numbers. I wanted to see an expression to achieve the same comparison in the absence of scalar types. Sorry if I should have figured this out for myself.

I'm grateful for the reminder that DEE is the identity under JOIN. So, with n-adic JOIN support we can write JOIN{} or JOIN() to denote REL{}{TUP{}}.

Hugh

Coauthor of The Third Manifesto and related books.

#53 · June 25, 2019, 1:56 am

Quote from Hugh on June 24, 2019, 1:34 pm

It never occurred to me that somebody might interpret my use of "replace" the way Antc has.

Thanks Hugh, then I am struggling to place any meaning on the question. Why would you ask about a comparison that is plainly false? Why wouldn't you just apply the definition I already gave (which of course has to differentiate equal operands from non-equal). I'll elide, for a crisp definition:

Equality-testing between scalars (i.e. singleton relations of degree one) corresponds thusly:

x == y =_df (REL{TUP{XY x}} JOIN REL{TUP{XY y}}) InnerUnion DUM

Then substute 1 = 2 into x == y, you get DUM aka FALSE.

With support for scalar type INTEGER I can write "1 = 2" to express comparison for equality on those two numbers. I wanted to see an expression to achieve the same comparison in the absence of scalar types. Sorry if I should have figured this out for myself.

I'm grateful for the reminder that DEE is the identity under JOIN. So, with n-adic JOIN support we can write JOIN{} or JOIN() to denote REL{}{TUP{}}.

DUM also has some nice identities: DUM = (x JOIN DUM) InnerUnion DUM = (x InnerUnion DUM) JOIN DUM for all x.

There's three ways to detect if a relation value is empty, using DUM:

x JOIN DUM = x; x InnerUnion DUM = DUM; x InnerUnion DUM /= DEE;

You can combine those (in)equalities to fix the definition of DUM in terms of JOIN.

The algebraist (for whom everything must be a relation) can use the emptied-out x JOIN DUM to represent the heading of x. Then two relations have the same heading just in case x JOIN DUM = y JOIN DUM. And traditional projection (of x on the attributes in common with y) is x InnerUnion (y JOIN DUM).

#54 · June 25, 2019, 9:19 am

In response to Antc:

I used "1 = 2" as about the simplest example of a legal expression denoting comparison that I can think of. I was frankly rather surprised that you should question its wisdom.

Anyway, your answer includes the expression TUP(XY x). That expression in Tutorial D is allowed on the assumption the declared type of x can be inferred by the system from that expression ("x"). For example, in Tutorial D, the system knows that the declared type of the expression "1" is INTEGER. So now I ask, without support for system-defined scalar types, how would you write an expression to have the same effect as TUP{XY INTEGER}{XY 1}?

Do I misunderstand what you mean by "relations only"?

(I do know all about TABLE_DUM, of course, being the one who first wrote about it and proposed its name, back in 1988.)

Hugh

Coauthor of The Third Manifesto and related books.

#55 · June 25, 2019, 10:17 am

Quote from Hugh on June 25, 2019, 9:19 am

In response to Antc:

I used "1 = 2" as about the simplest example of a legal expression denoting comparison that I can think of. I was frankly rather surprised that you should question its wisdom.

Thank you Hugh. No I wasn't questioning its wisdom. I was wondering why you didn't think the answer to the comparison was already given. So then I was trying to cast around for what other question you might have had in mind.

Anyway, your answer includes the expression TUP(XY x). That expression in Tutorial D is allowed on the assumption the declared type of x can be inferred by the system from that expression ("x"). For example, in Tutorial D, the system knows that the declared type of the expression "1" is INTEGER. So now I ask, without support for system-defined scalar types, how would you write an expression to have the same effect as TUP{XY INTEGER}{XY 1}?

I've despatched BOOL. Then why should there be any system-defined scalar types? Types are orthogonal to model. I daresay users might want to define some types, including INTEGER and other numerics. Those would be user-defined types.

Algebraical D would have a means to write relation literals. I can't see any difficulty allowing optional type annotations on attribute values. I'd also expect ways to write HHT 1975-style 'algorithmic relations', to implement things like Appendix A's PLUS, and those would need type annotations.

TUP{XY INTEGER} {XY 1} doesn't return a relation, so it's not well-formed stand-alone. It would have to appear inside REL{...} -- and we'd need to support type annotations on relation literals, especially to express the heading for empty relations.

Do I misunderstand what you mean by "relations only"?

(I do know all about TABLE_DUM, of course, being the one who first wrote about it and proposed its name, back in 1988.)

So did you persuade Codd of what it could be used for?

#56 · June 26, 2019, 11:08 am

Quote from AntC on June 25, 2019, 10:17 am

Quote from Hugh on June 25, 2019, 9:19 am

In response to Antc:

I used "1 = 2" as about the simplest example of a legal expression denoting comparison that I can think of. I was frankly rather surprised that you should question its wisdom.

Thank you Hugh. No I wasn't questioning its wisdom. I was wondering why you didn't think the answer to the comparison was already given. So then I was trying to cast around for what other question you might have had in mind.

Please try to understand why such examples are useful in discussions of language design. Variables would just complicate matters needlessly.

Anyway, your answer includes the expression TUP(XY x). That expression in Tutorial D is allowed on the assumption the declared type of x can be inferred by the system from that expression ("x"). For example, in Tutorial D, the system knows that the declared type of the expression "1" is INTEGER. So now I ask, without support for system-defined scalar types, how would you write an expression to have the same effect as TUP{XY INTEGER}{XY 1}?

I've despatched BOOL. Then why should there be any system-defined scalar types? Types are orthogonal to model. I daresay users might want to define some types, including INTEGER and other numerics. Those would be user-defined types.

Tutorial D relies on existing types in its support for UDT definitions. So do your restricted TUPLE{...} expressions. How do you get off the ground, so to speak, without any system-defined scalar types?

Hugh

Coauthor of The Third Manifesto and related books.

#57 · June 26, 2019, 2:59 pm

Quote from Hugh on June 26, 2019, 11:08 am

Tutorial D relies on existing types in its support for UDT definitions. So do your restricted TUPLE{...} expressions. How do you get off the ground, so to speak, without any system-defined scalar types?

It took me quite a while to figure this out too. In this particular mathematical game, a type A (with values a1, a2, ...) is said to be "reduced" or "eliminated" if there is a type B (with values b1, b2, ...) such that every value of A can be mapped onto a distinct value of B. In a further extension of language, people say that a1 , a2, ... are b1, b2, ....

The best-known example is probably the von Neumann reduction of natural numbers to sets. The mapping function here is 0 = {}, 1 = {0}, 2 = {1}, and so on. All the operations on natural numbers are mapped too: + is now an operation on (some) sets defined with the help of the successor (plus-one) function, which is justsucc x = {x}. Then addition is inductively (recursively) defined as:

a + 0 = a
a + succ b = succ(a + b)

which eventually reduces to succ succ succ ...a. There are other reductions as well, and you choose the one that is most convenient for your purpose. The laws of primary-school arithmetic do not change when the mapping changes.

Mathematicians don't worry about numbers being a fundamentally different type from sets. Indeed, the fewer root types they have, the happier they are.

#58 · June 26, 2019, 10:59 pm

Quote from AntC on June 26, 2019, 10:59 pm

Quote from Hugh on June 26, 2019, 11:08 am

Quote from AntC on June 25, 2019, 10:17 am

Quote from Hugh on June 25, 2019, 9:19 am

In response to Antc:

I used "1 = 2" as about the simplest example of a legal expression denoting comparison that I can think of. I was frankly rather surprised that you should question its wisdom.

Thank you Hugh. No I wasn't questioning its wisdom. I was wondering why you didn't think the answer to the comparison was already given. So then I was trying to cast around for what other question you might have had in mind.

Please try to understand why such examples are useful in discussions of language design. Variables would just complicate matters needlessly.

Anyway, your answer includes the expression TUP(XY x). That expression in Tutorial D is allowed on the assumption the declared type of x can be inferred by the system from that expression ("x"). For example, in Tutorial D, the system knows that the declared type of the expression "1" is INTEGER. So now I ask, without support for system-defined scalar types, how would you write an expression to have the same effect as TUP{XY INTEGER}{XY 1}?

I've despatched BOOL. Then why should there be any system-defined scalar types? Types are orthogonal to model. I daresay users might want to define some types, including INTEGER and other numerics. Those would be user-defined types.

Tutorial D relies on existing types

I'm clearly not talking about Tutorial D, or any semantics close to it. (I'm just borrowing its syntax, as the lingua franca round here.)

in its support for UDT definitions. So do your restricted TUPLE{...} expressions. How do you get off the ground, so to speak, without any system-defined scalar types?

(Thank you to John for his comment about purist mathematics/sets all the way down. Or I could make it lambda calculus all the way, with Church Encodings of types. But I'm not going that far.)

Consider the Haskell language, which is eminently practical and not purely theoretical. This comes with no system-defined types. Various parts of the syntax expect certain types, for example
if p then e1 else e2; -- is syntactic sugar for

case p of
  { True -> e1;
    False -> e2
  }
The case construct can be used for whatever type of scrutinee, of which the branches must be the possible values within the type. So does the if then else construct mean that Bool must be system-defined?

No, a user can supply their own definitions of True, False, and the type they belong to (which doesn't have to be called Bool and doesn't necessarily have exactly two member values, and doesn't even have to have the interpretation you'd expect of True, False). Or a user can merely avoid the if then else construct.

Similarly the syntax defines formats for sequences of digits and sequences of digits with one included .. You can interpret those as Integer and Floating point respectively if you choose to -- or you can build your own Numeric types upon it. Specifically, 1234 appearing as a language token is shorthand for fromInteger 1234 where fromInteger must be a user-defined function, returning a value of type within the Num class -- which must be user-supplied, and which usually would include user-definitions for the usual mathematical operators.

Does Haskell just 'leave you in the lurch' like that? Well no, it comes with comprehensive libraries with all the usual stuff pre-defined. But the point is those libraries/types defined are no different to user-defined libraries/types, and indeed you can pick and choose between them; you can edit them to arrive at your own definitions. That's what I mean by 'type orthogonal to model'.

Types "get of the ground " because type declarations introduce both the type name and names for all the member values. The full generality of type declarations allows building types from already-defined types (as with Tutorial D user-defined types), but you need to start with the boot laces.
data Bool = False | True;
is the (usual/library-supplied) declaration for type-name Bool (the definiens) with member values False, True (sequenced that way round so that False evaluates to less than True). The keyword data (which you've complained about before: why not type?) is because False, True are data values. (Other declarations declare for example type aliases, which don't mention data values.)

The | separator between the member values is introducing a 'sum type' aka 'tagged union', as in sum-of-product types. It is (theoretically) how all base types are defined
data Int = -9223372036854775808 | ... | -2 | -1 | 0 | 1 | 2 | ... | 9223372036854775807

data Char = '\NUL' | ... | ' ' | 'A' | 'B' | ... | 'a' | 'b' | ... '\1114111'
One small detail: sum-of-product types are declared to have a fixed number of components (with each component of fixed type). So this doesn't apply for REL{ }, TUP{ } because they are variadic, furthermore we can permute the components inside those { } to get equivalent expressions. We'd have to treat those as hard-coded syntax. Note that Haskell does have tuples as fixed-order sequences, more like traditional math:
data (,) alpha beta = (alpha, beta)
data (,,) alpha beta gamma = (alpha, beta, gamma)
...
alpha, beta are type variables, showing these definitions are polymorphic: you can build tuples out of any types at all, not necessarily the same.

Quote from Hugh on June 26, 2019, 11:08 am

Quote from AntC on June 25, 2019, 10:17 am

Quote from Hugh on June 25, 2019, 9:19 am

In response to Antc:

I used "1 = 2" as about the simplest example of a legal expression denoting comparison that I can think of. I was frankly rather surprised that you should question its wisdom.

Thank you Hugh. No I wasn't questioning its wisdom. I was wondering why you didn't think the answer to the comparison was already given. So then I was trying to cast around for what other question you might have had in mind.

Please try to understand why such examples are useful in discussions of language design. Variables would just complicate matters needlessly.

Anyway, your answer includes the expression TUP(XY x). That expression in Tutorial D is allowed on the assumption the declared type of x can be inferred by the system from that expression ("x"). For example, in Tutorial D, the system knows that the declared type of the expression "1" is INTEGER. So now I ask, without support for system-defined scalar types, how would you write an expression to have the same effect as TUP{XY INTEGER}{XY 1}?

I've despatched BOOL. Then why should there be any system-defined scalar types? Types are orthogonal to model. I daresay users might want to define some types, including INTEGER and other numerics. Those would be user-defined types.

Tutorial D relies on existing types

I'm clearly not talking about Tutorial D, or any semantics close to it. (I'm just borrowing its syntax, as the lingua franca round here.)

in its support for UDT definitions. So do your restricted TUPLE{...} expressions. How do you get off the ground, so to speak, without any system-defined scalar types?

(Thank you to John for his comment about purist mathematics/sets all the way down. Or I could make it lambda calculus all the way, with Church Encodings of types. But I'm not going that far.)

Consider the Haskell language, which is eminently practical and not purely theoretical. This comes with no system-defined types. Various parts of the syntax expect certain types, for example

if p then e1 else e2; -- is syntactic sugar for

case p of
  { True -> e1;
    False -> e2
  }

The case construct can be used for whatever type of scrutinee, of which the branches must be the possible values within the type. So does the if then else construct mean that Bool must be system-defined?

No, a user can supply their own definitions of True, False, and the type they belong to (which doesn't have to be called Bool and doesn't necessarily have exactly two member values, and doesn't even have to have the interpretation you'd expect of True, False). Or a user can merely avoid the if then else construct.

Similarly the syntax defines formats for sequences of digits and sequences of digits with one included .. You can interpret those as Integer and Floating point respectively if you choose to -- or you can build your own Numeric types upon it. Specifically, 1234 appearing as a language token is shorthand for fromInteger 1234 where fromInteger must be a user-defined function, returning a value of type within the Num class -- which must be user-supplied, and which usually would include user-definitions for the usual mathematical operators.

Does Haskell just 'leave you in the lurch' like that? Well no, it comes with comprehensive libraries with all the usual stuff pre-defined. But the point is those libraries/types defined are no different to user-defined libraries/types, and indeed you can pick and choose between them; you can edit them to arrive at your own definitions. That's what I mean by 'type orthogonal to model'.

Types "get of the ground " because type declarations introduce both the type name and names for all the member values. The full generality of type declarations allows building types from already-defined types (as with Tutorial D user-defined types), but you need to start with the boot laces.

data Bool = False | True;

is the (usual/library-supplied) declaration for type-name Bool (the definiens) with member values False, True (sequenced that way round so that False evaluates to less than True). The keyword data (which you've complained about before: why not type?) is because False, True are data values. (Other declarations declare for example type aliases, which don't mention data values.)

The | separator between the member values is introducing a 'sum type' aka 'tagged union', as in sum-of-product types. It is (theoretically) how all base types are defined

data Int = -9223372036854775808 | ... | -2 | -1 | 0 | 1 | 2 | ... | 9223372036854775807

data Char = '\NUL' | ... | ' ' | 'A' | 'B' | ... | 'a' | 'b' | ... '\1114111'

One small detail: sum-of-product types are declared to have a fixed number of components (with each component of fixed type). So this doesn't apply for REL{ }, TUP{ } because they are variadic, furthermore we can permute the components inside those { } to get equivalent expressions. We'd have to treat those as hard-coded syntax. Note that Haskell does have tuples as fixed-order sequences, more like traditional math:

data (,) alpha beta = (alpha, beta)
data (,,) alpha beta gamma = (alpha, beta, gamma)
...

alpha, beta are type variables, showing these definitions are polymorphic: you can build tuples out of any types at all, not necessarily the same.

#59 · June 27, 2019, 7:01 am

Quote from Dave Voorhis on June 27, 2019, 7:01 am
Quote from AntC on June 26, 2019, 10:59 pm

Quote from Hugh on June 26, 2019, 11:08 am

in its support for UDT definitions. So do your restricted TUPLE{...} expressions. How do you get off the ground, so to speak, without any system-defined scalar types?

...

Types "get of the ground " because type declarations introduce both the type name and names for all the member values. The full generality of type declarations allows building types from already-defined types (as with Tutorial D user-defined types), but you need to start with the boot laces.
data Bool = False | True;
data Bool = False | True;
data Bool = False | True;
is the (usual/library-supplied) declaration for type-name Bool (the definiens) with member values False, True (sequenced that way round so that False evaluates to less than True). The keyword data (which you've complained about before: why not type?) is because False, True are data values. (Other declarations declare for example type aliases, which don't mention data values.)

The | separator between the member values is introducing a 'sum type' aka 'tagged union', as in sum-of-product types. It is (theoretically) how all base types are defined
data Int = -9223372036854775808 | ... | -2 | -1 | 0 | 1 | 2 | ... | 9223372036854775807

data Char = '\NUL' | ... | ' ' | 'A' | 'B' | ... | 'a' | 'b' | ... '\1114111'
data Int = -9223372036854775808 | ... | -2 | -1 | 0 | 1 | 2 | ... | 9223372036854775807

data Char = '\NUL' | ... | ' ' | 'A' | 'B' | ... | 'a' | 'b' | ... '\1114111'
If the above is "(theoretically) how all base types are defined", how are base types like Int and Char actually defined?

Is it compiler magic (i.e., baked into the compiler), or do definitions like the above for Int and Char live somewhere in the Haskell standard library (or equivalent)?

Either way, the answer to Hugh's question ("How do you get off the ground, so to speak, without any system-defined scalar types?") appears to be that numeric and character literals are special, baked into the compiler, and at least (if it's the latter case) predefined (by the compiler) to be notionally "typeful" to the extent that, for example, -9223372036854775808 | ... | -2 is recognised to represent a range of ordinal numeric values.

Or is that not how it works?

Quote from AntC on June 26, 2019, 10:59 pm

Quote from Hugh on June 26, 2019, 11:08 am

in its support for UDT definitions. So do your restricted TUPLE{...} expressions. How do you get off the ground, so to speak, without any system-defined scalar types?

...

Types "get of the ground " because type declarations introduce both the type name and names for all the member values. The full generality of type declarations allows building types from already-defined types (as with Tutorial D user-defined types), but you need to start with the boot laces.
data Bool = False | True;
data Bool = False | True;
data Bool = False | True;
is the (usual/library-supplied) declaration for type-name Bool (the definiens) with member values False, True (sequenced that way round so that False evaluates to less than True). The keyword data (which you've complained about before: why not type?) is because False, True are data values. (Other declarations declare for example type aliases, which don't mention data values.)

The | separator between the member values is introducing a 'sum type' aka 'tagged union', as in sum-of-product types. It is (theoretically) how all base types are defined
data Int = -9223372036854775808 | ... | -2 | -1 | 0 | 1 | 2 | ... | 9223372036854775807

data Char = '\NUL' | ... | ' ' | 'A' | 'B' | ... | 'a' | 'b' | ... '\1114111'
data Int = -9223372036854775808 | ... | -2 | -1 | 0 | 1 | 2 | ... | 9223372036854775807

data Char = '\NUL' | ... | ' ' | 'A' | 'B' | ... | 'a' | 'b' | ... '\1114111'

If the above is "(theoretically) how all base types are defined", how are base types like Int and Char actually defined?

Is it compiler magic (i.e., baked into the compiler), or do definitions like the above for Int and Char live somewhere in the Haskell standard library (or equivalent)?

Either way, the answer to Hugh's question ("How do you get off the ground, so to speak, without any system-defined scalar types?") appears to be that numeric and character literals are special, baked into the compiler, and at least (if it's the latter case) predefined (by the compiler) to be notionally "typeful" to the extent that, for example, -9223372036854775808 | ... | -2 is recognised to represent a range of ordinal numeric values.

Or is that not how it works?

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

#60 · June 27, 2019, 10:53 am

Thanks for the attempts to answer my question, "How do you get off the ground?", from John, Antc, and Dave Voorhis.

I did attempt to adduce von Neumann's axioms (without mentioning the name because I wasn't sure who was the originator, having the name "Peano" uncertainly in mind) in an early contribution to this thread, but I wasn't sure that type INTEGER would be sufficient for everything else. I am of course aware of the famous quote, "Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk" ("God made the integers, all else is the work of man" - thanks to Wikipedia for the original German and for telling me who made it), but does it answer my question? If so, I'm close to being convinced that the final sentence of RM Pre 1 is theoretically redundant but I wouldn't wish to delete it, considering SQL's lack of support for it. After all it was SQL (mostly) that led us to write TTM in the first place. Also, TTM is about language design, so it seemed reasonable to me to question whether it was feasible to design a computer language embracing Antc's hypothesis: given DEE and DUM, we can define some scalar types, including BOOLEAN, as UDTs, and then all relation types of degree >0 fall into place (as I understand it).

Dave asks how types int and char are actually defined. Those were the questions in my mind, too. Antc offers some concrete syntax based on Tutorial D but shies away from getting down to brass tacks. As I don't feel up to it myself I would be most grateful it somebody else can do it, preferably in TD style.

By the way, an idle remark: some textbooks define an n-tuple as a function, mapping names to values, and a function is a slightly special case of a relation.

Hugh

Coauthor of The Third Manifesto and related books.

The Forum for Discussion about The Third Manifesto and Related Matters