Which type?

#1 · November 10, 2021, 1:26 pm

Quote from Paul Vernon on November 10, 2021, 1:26 pm
It is said that

A value necessarily brings a type

We require typed sets

attributes [in turn] have types

All scalar values shall be typed—i.e., such values shall always carry with them, at least conceptually, some identification of the type to which they belong.

since the value, variable, and operator concepts in turn all rely on the type concept, we might go further and say the type concept can be regarded as a foundation for the foundation for the foundation ...

In other words, the type concept is the most fundamental of all

However this is all really just an axiom of a particular model. I find no justification for this axiom - only appeals to "type safety" and maybe "common sense".

The FAQ section of CJD's Logic and Databases has an "answer" to the explain the last bullet above. But to my mind it gives no such answer. Indeed CJD is honest enough to outline an argument (which he finds "a little troubling") for the position that "all we need is values".

Axiomatically assuming (at least some) atomic values exists is compelling. Assuming there is a way to "collect" values (as members) into a "set" of some kind is also compelling. However the need to give each value a type (or many types with type inheritance), is very much less so to me.

In other words, why must values carry with them a type? (Why can't they just be)

If we can have "safety" without axiomatic types, then types can just be any old (named) sets of values, rather than something foundational

And who gets to define these types anyway? Why is the prime numbers (to pick one example) not a type (or is it :-)?

P.S. I apologise if this is "old ground" - well, I know it is old ground - and I don't want to spark a long debate especially about "type safety" (including in the broadest sense such as "safety" mechanisms to allow us to sidestep e.g. Russell's Paradox) or "type systems" ... but I've done a fair bit of reading, but I'm still to find really good reasons why types might necessarily be foundational (apart from reasons of safety as I think there are/should be other ways of tackling that)

It is said that

A value necessarily brings a type
We require typed sets
attributes [in turn] have types
All scalar values shall be typed—i.e., such values shall always carry with them, at least conceptually, some identification of the type to which they belong.
since the value, variable, and operator concepts in turn all rely on the type concept, we might go further and say the type concept can be regarded as a foundation for the foundation for the foundation ...
In other words, the type concept is the most fundamental of all

However this is all really just an axiom of a particular model. I find no justification for this axiom - only appeals to "type safety" and maybe "common sense".

The FAQ section of CJD's Logic and Databases has an "answer" to the explain the last bullet above. But to my mind it gives no such answer. Indeed CJD is honest enough to outline an argument (which he finds "a little troubling") for the position that "all we need is values".

Axiomatically assuming (at least some) atomic values exists is compelling. Assuming there is a way to "collect" values (as members) into a "set" of some kind is also compelling. However the need to give each value a type (or many types with type inheritance), is very much less so to me.

In other words, why must values carry with them a type? (Why can't they just be)

If we can have "safety" without axiomatic types, then types can just be any old (named) sets of values, rather than something foundational

And who gets to define these types anyway? Why is the prime numbers (to pick one example) not a type (or is it :-)?

P.S. I apologise if this is "old ground" - well, I know it is old ground - and I don't want to spark a long debate especially about "type safety" (including in the broadest sense such as "safety" mechanisms to allow us to sidestep e.g. Russell's Paradox) or "type systems" ... but I've done a fair bit of reading, but I'm still to find really good reasons why types might necessarily be foundational (apart from reasons of safety as I think there are/should be other ways of tackling that)

#2 · November 10, 2021, 4:21 pm

Why a value has to have a single type attached to it, not many? The eternal "is square inherited from rectangle" debate hints that probably there has to be many. Then, as soon as we agreed that there are the two disjoint sets: objects and types, and the connection between them "an object x is associated with type T", then we can frame that tiresome "is square inherited from rectangle" debate into the Formal Concept Analysis. From that perspective a hierarchy of types is formally a lattice.

The other side of your question is why more than one type is needed for a database. IMO, an RDBMS which manipulates string values exclusively is perfectly fine. I would even argue that it is exactly the system that fits for teaching the Database introductory class.

#3 · November 10, 2021, 6:02 pm

My question was actually why does a (atomic) value have to have any type attached to it.

Giving a value just one type is argued against by type inheritance, but then we get to question of how many types should a given value have. The value 2 is of type Integer, Rational, Real, Prime, Even, Positive, Imaginary etc. I'm not sure that such a multitude should be axiomatic. If one and many are both discounted, that just leaves zero as the answer to the question of how many types does an atomic value "always carry with them".

P.S. I certainly would not advocate "only strings". Even (maybe even especially) in a teaching system, we want true and false , 0, 1, 2 etc as atomic values.

#4 · November 10, 2021, 8:08 pm

Quote from AntC on November 10, 2021, 8:08 pm

Quote from Paul Vernon on November 10, 2021, 6:02 pm

My question was actually why does a (atomic) value have to have any type attached to it.

There's various ways to define type systems. What TTM assumes is called 'nominal typing'. You could argue on a point of terminological/historical nitpicking that under different approaches, it would be jolly helpful not to call all these things 'types', but we are where we are.

Haskell programming language also has what it calls nominal typing. It's different to TTM's definition. In Haskell you go (for example):

data Bool = True | False;

This brings into existence three names: a type Bool and two values. The values cannot exist unless they are introduced via a type. (The compiler chooses what will be the hardware representation for those values. Contrast for example that ALGOL 68 allows you to specify the hardware rep for a value of a type.) So yes, atomic values must have a type attached. (Really I want a stronger word than "attached": intrinsic to.) Structured values must have a structure of types. In Haskell there is no type inheritance in the sense of values belonging to more than one type. If you want a type to represent non-negative Integers, you can't just declare it as a subset of Integers.

TTM assumes there's already a given universe of values. And TTM has already ordained what are its primitive types, and which of the given values belong to which type. I find that far less appealing, because it gives rise to questions like "why does a atomic value have to have any type attached to it". And "how many types should a given value have" -- which also makes it hard work for the compiler: does bare 5 mean Integer 5 or non-negative Integer 5?

Giving a value just one type is argued against by type inheritance, but then we get to question of how many types should a given value have. The value 2 is of type Integer, Rational, Real, Prime, Even, Positive, Imaginary etc. I'm not sure that such a multitude should be axiomatic.

Here you're mixing up two things: the underlying value and its type vs. the program-text representation thereof. The Haskell approach is that 2 appearing in program text denotes a polymorphic (niladic) function whose result is an underlying value of some specific type, when the program text gives it a signature, or when it appears in a context sufficient to resolve to a type. Haskell arrived at this approach in 1989 in an email from Phil Wadler. You can practically see the lightbulb switching on, because this solves so many problems in so many programming languages. (If you want specifically short Int 2, you can write that 2#. But for most numeric types there's no shorthand textual representation, you give a type annotation: 2 :: Integer, 2.0 :: Float, 2.0 :: Double, .... A non-negative Integer is typically represented in program text as a structured value, maybe (NonNegInteger 2), even though its underlying machine representation is exactly the same as 2 :: Integer.

If one and many are both discounted, that just leaves zero as the answer to the question of how many types does an atomic value "always carry with them".

P.S. I certainly would not advocate "only strings". Even (maybe even especially) in a teaching system, we want true and false , 0, 1, 2 etc as atomic values.

I should perhaps add that I find TTM's Type Inheritance model a nonsense riddled with confusions such as you are raising. "how many types should a given value have" -- under TTM Inheritance, the answer is up to the number of powersets you can build over the values in its 'base type'.

Quote from Paul Vernon on November 10, 2021, 6:02 pm

My question was actually why does a (atomic) value have to have any type attached to it.

There's various ways to define type systems. What TTM assumes is called 'nominal typing'. You could argue on a point of terminological/historical nitpicking that under different approaches, it would be jolly helpful not to call all these things 'types', but we are where we are.

Haskell programming language also has what it calls nominal typing. It's different to TTM's definition. In Haskell you go (for example):

data Bool = True | False;

This brings into existence three names: a type Bool and two values. The values cannot exist unless they are introduced via a type. (The compiler chooses what will be the hardware representation for those values. Contrast for example that ALGOL 68 allows you to specify the hardware rep for a value of a type.) So yes, atomic values must have a type attached. (Really I want a stronger word than "attached": intrinsic to.) Structured values must have a structure of types. In Haskell there is no type inheritance in the sense of values belonging to more than one type. If you want a type to represent non-negative Integers, you can't just declare it as a subset of Integers.

TTM assumes there's already a given universe of values. And TTM has already ordained what are its primitive types, and which of the given values belong to which type. I find that far less appealing, because it gives rise to questions like "why does a atomic value have to have any type attached to it". And "how many types should a given value have" -- which also makes it hard work for the compiler: does bare 5 mean Integer 5 or non-negative Integer 5?

Giving a value just one type is argued against by type inheritance, but then we get to question of how many types should a given value have. The value 2 is of type Integer, Rational, Real, Prime, Even, Positive, Imaginary etc. I'm not sure that such a multitude should be axiomatic.

Here you're mixing up two things: the underlying value and its type vs. the program-text representation thereof. The Haskell approach is that 2 appearing in program text denotes a polymorphic (niladic) function whose result is an underlying value of some specific type, when the program text gives it a signature, or when it appears in a context sufficient to resolve to a type. Haskell arrived at this approach in 1989 in an email from Phil Wadler. You can practically see the lightbulb switching on, because this solves so many problems in so many programming languages. (If you want specifically short Int 2, you can write that 2#. But for most numeric types there's no shorthand textual representation, you give a type annotation: 2 :: Integer, 2.0 :: Float, 2.0 :: Double, .... A non-negative Integer is typically represented in program text as a structured value, maybe (NonNegInteger 2), even though its underlying machine representation is exactly the same as 2 :: Integer.

If one and many are both discounted, that just leaves zero as the answer to the question of how many types does an atomic value "always carry with them".

P.S. I certainly would not advocate "only strings". Even (maybe even especially) in a teaching system, we want true and false , 0, 1, 2 etc as atomic values.

I should perhaps add that I find TTM's Type Inheritance model a nonsense riddled with confusions such as you are raising. "how many types should a given value have" -- under TTM Inheritance, the answer is up to the number of powersets you can build over the values in its 'base type'.

#5 · November 10, 2021, 8:27 pm

To me,2 appearing in program text denotes, well, the value 2. I'm not sure I need any more complexity than that.

BTW I would not allow any other thing to denote the value 2. Not 02 nor 2.0 nor +2 nor ²⁄₁ nor 2+0i nor, for that matter 1+1

#6 · November 10, 2021, 8:42 pm

Quote from Paul Vernon on November 10, 2021, 8:27 pm

To me,2 appearing in program text denotes, well, the value 2. I'm not sure I need any more complexity than that.

BTW I would not allow any other thing to denote the value 2. Not 02 nor 2.0 nor +2 nor ²⁄₁ nor 2+0i nor, for that matter 1+1

No expressions?

Do you allow strings, like '2'?

Is 2 equal to '2'?

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

#7 · November 10, 2021, 9:52 pm

Expressions sure. 1+1 evaluates to 2, it is not the same as 2

Strings? Sure. "A" , "2" etc.

Is 2 equal to"2"? Well (obviously?) not. As I said, I would not allow two ways to denote (i.e. have two different literals for) the same thing (not within a given universe of discourse anyway).

P.S. I'm assuming we're taking equal to mean "is the same or evaluates to the same", and reserve "same" for well, "is the same" (I could say identical, but that means the same as same, right?). No matter, "2" is (to me) neither the same as, nor does it evaluate to 2

#8 · November 10, 2021, 10:14 pm

Quote from Paul Vernon on November 10, 2021, 9:52 pm

Expressions sure. 1+1 evaluates to 2, it is not the same as 2

So 1 + 1 ≠ 2 ?

Strings? Sure. "A" , "2" etc.

Is 2 equal to"2"? Well (obviously?) not. As I said, I would not allow two ways to denote (i.e. have two different literals for) the same thing (not within a given universe of discourse anyway).

P.S. I'm assuming we're taking equal to mean "is the same or evaluates to the same", and reserve "same" for well, "is the same" (I could say identical, but that means the same as same, right?). No matter, "2" is (to me) neither the same as, nor does it evaluate to 2

Sounds like you're describing a type system.

I'm not convinced it's entirely sound (it sounds like 1 + 1 ≠ 2) but I'm not sure that matters. Unsoundness doesn't seem to have stopped JavaScript.

Or SQL, for that matter.

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

#9 · November 10, 2021, 11:04 pm

I would use = as per normal practice and have both sides evaluated before doing the comparison.

A type system? Not really. Sure I would have a set of strings and "a" would be a member, but I'ld also have a set of English dictionary words, and "a" would be a member of that too, but not all members of the string set would be members of the word set. I'ld have a subset of strings that correspond to "valid Unicode code-point sequences", and many other interesting subsets of the string set.

What I would not do is point to one set and say "that set is a type" and another set and say "that set is not a type". Not in any fundamental way anyway. I mean a user might say "what types of values does your database support, and we might reply with, well we have sets, ordered pairs and the atoms from the following non-overlapping named sets: booleans, bits, integers, non-integer-rationals, non-rational-constructable-reals, valid-unicode-strings, invaild-unicode-codpoint-sequences, etc etc. We might even go so far as to say those sets define the "type" of a value, but I'm pretty sure you could not accuse such a thing as being a "type system" (If you can, well, then I guess I am guilty of having a type system even if all that means is that there exists two or more sets that partition the atomic values)

P.S. I get a perverse encouragement from existing unsound systems. If I built a system that turned out to be unsound, that might not actually stop it from being useful (even if it would surly limit its usefulness in some way.) Still, obviously (?!) it is hugely preferable for a system to be sound...

#10 · November 11, 2021, 12:48 am

The RM does not require a type system. It is enough to have definitions for relations, tuples, attributes and values. If the values are of some type, the RM does not need to know.

The RA does not require a type system, but it does need to be able to test values for equality.

The ERA depends on relcons, Any implementation of a relcon will necessarily depend on the concept of type, but that is all.

A programming language that seeks to incorporate the RM and ERA will necessarily require a mapping to a type system.

In all the database models I can ever remember seeing, I have never found the need for more than 9 scalar types: boolean, integer, real, decimal, datetime, text string, binary string, enum, struct. (And I regard value inheritance as a pointless thought experiment.)

A programming language may have many more types, but IMO it should support those 9 as scalar value types if it is to be a database programming language (which is the aim of TTM/D). I don't know any that do.

Andl - A New Database Language - andl.org

The Forum for Discussion about The Third Manifesto and Related Matters

Which type?