The Forum for Discussion about The Third Manifesto and Related Matters

Please or Register to create posts and topics.

Specialisation-by-Constraint for arithmetic operations: up to a point, Lord Copper

(I continue to be unmoved by the examples of geometric figures in TTM's discussion of S-by-C; I'd like to narrow to arithmetic operations, as more applicable.)

I'll start by saying I'm fully up with the TTM programme w.r.t. database constraints:

  • RM Pre 23 "D shall provide facilities for defining and destroying integrity constraints (constraints for short)."
  • RM Pre 15 "Every relvar shall have at least one candidate key."
  • RM VSS 2 "the system to be able to infer the candidate keys of R [the result from a relational expression]"
  • I'd even go beyonf RM VSS 2 to suggest the system try to infer integrity constraints in general for the result from a relational expression or from a scalar expression; the idea being to statically determine that some update to a relvar is guaranteed to preserve constraints. Saying "try to" means I realise the problem is in general undecidable.

I'll also say that the "three out of four rule"/argument doesn't persuade me at all: of the four, I do not anyway want to support reference semantics nor type-changing mutability; so for me it's a three-out-of-three rule.

Much of the OOP argument for what they call 'inheritance' is Specialisation-by-Extension/structural sub-typing; for which TTM has a ready answer: auxiliary relvars.

Then I'm going to consider S-by-C for arithmetic operations, specifically over Integers, constrained types: POSINT, NONNEGINT.

  • A program could constrain a divisor to be POSINT, thereby using the type system to avoid divide-by-zero.
  • Is this useful? In particular, if the divisor is an expression (á  la RM VSS2) can the type system derive that the result could never be zero?
  • Suppose the divisor expression is a multiplication: it'd require both factors be POSINT, so far so good.
  • Suppose the divisor expression is an addition: it'd require at least one summand to be POSINT, the other could be NONNEGINT, not so good.
  • Suppose the divisor expression is a subtraction: it'd require the minuend be strictly greater than the subtrahend. That's not a type-characteristic of either operand, no good at all.
  • Then suppose the divisor is a subtraction for which the subtrahend is a multiplication: it's fine to produce zero from that multiplication, no need to constrain the factors to be POSINT; this is getting well beyond what type inference can typically cope with.

 

  • Likewise if we were trying to constrain integer division to always produce an integer result: that's not a type-characteristic of either operand individually.
  • Likewise trying to type-constrain arithmetic operations to avoid arithmetic over/underflow.
  • Etc.

So this is my difficulty with the claim that 'dynamic typing' is a type system: if some language wants to classify divide-by-zero as a type error -- as opposed to just any old run-time exception -- a S-by-C POSINT can't 'reach out' through type-solving to the rest of the program to avoid run-time exceptions. That is, in general: there are some programs it can see would never produce a zero divisor; there are many for which it could only see they might/not produce a zero divisor; and this is not bumping into the constraint-inference is undecidable issue; it can happen with quite easily inferrable constraints.

And isn't this a general limitation on S-by-C? Statically it is not possible to determine that a program will preserve constraints. Then there's always a possibility a (allegedly) well-typed program can still 'go wrong' -- that is, throw a run-time exception. Then classifying that exception as a type-error strikes me as unhelpful playing with semantics.

That is, one of the three-out-of-three: Static type checking we get by shifting the semantics, but not achieving the spirit of 'well-typed programs can't go wrong'.

Then I'm just not seeing the merit of S-by-C. Indeed it would be better if the TTM Selector for POSINT actually executed some code to check its argument was positive. IOW if a Selector were a 'Constructor' by that thrice-accursed definition.

Quote from AntC on June 13, 2020, 5:59 am

[...]

Much of the OOP argument for what they call 'inheritance' is Specialisation-by-Extension/structural sub-typing; for which TTM has a ready answer: auxiliary relvars.

What are auxiliary relvars?

I just searched for "auxiliary" in DTATRM and DBE, and found only one (completely unrelated) instance of the word in DBE.

I note that an awful lot of discussion about inheritance misunderstands how it should be used in object oriented programming, which I mention because that's where specialisation-by-extension holds sway. (If that's not at all where you were going with mention of S-by-E, then my apologies.)

The usual object-oriented inheritance examples typically involve peculiar real-world domain taxonomies -- zoo animals and vehicles and the like -- that are nothing like real programming hierarchies.

In real object-oriented programming, inheritance hierarchies are used to describe computational mechanisms that are hierarchical by levels of abstraction, rather than by contents of data structure.

For example, a typical hierarchy might start with a base class or interface called Report which defines the characteristics of all reports.

Inherited from Report might be SectionedReport, which defines reports with headings and footers and sections.

Inherited from SectionedReport might be ColumnarReport, which is a report with columns and headings and footers and sections.

Inherited from ColumnarReport might be TrialBalance, which is an application-specific report with a title heading, blank footer, and account-type sections and account & debit & credit columns with a grand total.

And so on.

Good object-oriented programming strongly encourages the programmer to then code to the highest level of abstraction possible. In other words, the programmer should reference Report wherever possible and reference TrialBalance as little as possible.

Good object-oriented programming also strongly encourages the programmer to make all subclasses of a superclass substitutable for the superclass. In other words, all subclasses of Report should behave equivalently as a Report. This is the Liskov Substitution Principle.

Done properly, and in general, you code algorithms to abstractions. In other words, you write algorithms to work with base classes or interfaces, then you implement concrete classes that define enough specific functionality to make the algorithms useful.

I mention all this only to point out that I'm not sure where relvars of any kind -- auxiliary or otherwise -- fit it into that. In general, object oriented programming -- including (and perhaps in particular) its inheritance hierarchies -- are about structuring code, not data. As such, data-driven S-by-C inheritance is categorically distinct and unrelated to code-driven structural inheritance. Indeed, I would thus expect them to be compatible but not overlapping; usable together or apart as appropriate to solve completely different problems -- one set of problems related to structuring data, another set of problems related to structuring code -- in a hypothetical D.

Then I'm going to consider S-by-C for arithmetic operations, specifically over Integers, constrained types: POSINT, NONNEGINT.

  • A program could constrain a divisor to be POSINT, thereby using the type system to avoid divide-by-zero.
  • Is this useful? In particular, if the divisor is an expression (á  la RM VSS2) can the type system derive that the result could never be zero?
  • Suppose the divisor expression is a multiplication: it'd require both factors be POSINT, so far so good.
  • Suppose the divisor expression is an addition: it'd require at least one summand to be POSINT, the other could be NONNEGINT, not so good.
  • Suppose the divisor expression is a subtraction: it'd require the minuend be strictly greater than the subtrahend. That's not a type-characteristic of either operand, no good at all.
  • Then suppose the divisor is a subtraction for which the subtrahend is a multiplication: it's fine to produce zero from that multiplication, no need to constrain the factors to be POSINT; this is getting well beyond what type inference can typically cope with.
  • Likewise if we were trying to constrain integer division to always produce an integer result: that's not a type-characteristic of either operand individually.
  • Likewise trying to type-constrain arithmetic operations to avoid arithmetic over/underflow.
  • Etc.

So this is my difficulty with the claim that 'dynamic typing' is a type system: if some language wants to classify divide-by-zero as a type error -- as opposed to just any old run-time exception -- a S-by-C POSINT can't 'reach out' through type-solving to the rest of the program to avoid run-time exceptions. That is, in general: there are some programs it can see would never produce a zero divisor; there are many for which it could only see they might/not produce a zero divisor; and this is not bumping into the constraint-inference is undecidable issue; it can happen with quite easily inferrable constraints.

And isn't this a general limitation on S-by-C? Statically it is not possible to determine that a program will preserve constraints. Then there's always a possibility a (allegedly) well-typed program can still 'go wrong' -- that is, throw a run-time exception. Then classifying that exception as a type-error strikes me as unhelpful playing with semantics.

That is, one of the three-out-of-three: Static type checking we get by shifting the semantics, but not achieving the spirit of 'well-typed programs can't go wrong'.

Then I'm just not seeing the merit of S-by-C. Indeed it would be better if the TTM Selector for POSINT actually executed some code to check its argument was positive. IOW if a Selector were a 'Constructor' by that thrice-accursed definition.

I wonder if S-by-C might be (better) replaced with predicate dispatch. In other words, rather than defining something like:

TYPE NONZERO IS INT CONSTRAINT VALUE != 0;
TYPE ZERO IS INT CONSTRAINT VALUE = 0;

OPERATOR DIV(X INT, Y NONZERO) RETURNS INT;
  RETURN X / Y;
END;

OPERATOR DIV(X INT, Y ZERO) RETURNS INT;
  THROW "Divide by zero (not really) averted!"
END;

Maybe better like:

OPERATOR DIV(X INT, Y INT) RETURNS INT CONSTRAINT Y != 0;
  RETURN X / Y;
END;

OPERATOR DIV(X INT, Y INT) RETURNS INT CONSTRAINT Y = 0;
  THROW "Divide by zero (not really) averted!";
END;

But that's not what you mean, is it?

And was S-by-C intended to eliminate run-time exceptions?

 

 

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 June 13, 2020, 10:34 am
Thank you Dave for your thoughtful replies. To answer your last point first:

And was S-by-C intended to eliminate run-time exceptions?

No type system eliminates run-time exceptions; with ALGOL-like or Haskell typing you still get divide-by-zero or numeric over/underflow. So no I'm not expecting S-by-C to eliminate all run-time exceptions.

Type systems for numeric types are supposed to statically guarantee you don't (for example) add an INT to a FLOAT and expect an INT result; as opposed to getting a runtime exception when trying to assign a FLOAT result that's non-integral. So if POSINT is a type distinct from INT, I'd expect (if there's any point in S-by-C) It would statically guarantee you'd never divide by zero. I'm failing to see that shunting a divide-by-zero runtime exception into a assign-zero-to-POSINT type error runtime exception is any more than playing with semantics. (I have seen that claimed on this forum and in the endless language wars as a benefit for dynamic typing. I'm not engaging in the (IMO fruitless) debate whether dynamic typing is just deferred static typing: in case of divide-by-zero, it usually can only be at runtime.)

 

Quote from AntC on June 13, 2020, 5:59 am

[...]

Much of the OOP argument for what they call 'inheritance' is Specialisation-by-Extension/structural sub-typing; for which TTM has a ready answer: auxiliary relvars.

What are auxiliary relvars?

What DBE Ch 23/The Decomposition Approach to 'Missing Information' arrives at by Vertical Decomposition/6NF. A toll bridge is a bridge that charges a toll; there's a base relvar holding bridge details (for all varieties of bridges); there's an auxiliary relvar that holds toll details, just for toll bridges. A Manager is an employee who manages a department; there's an employee relvar; there's an auxiliary relvar for managers identifying the department; if an EmployeeId appears in the employee relvar but not the manages-department auxiliary relvar, that is a non-manager employee.

This is the sort of subset-typing (Managers are a subset of Employees) that Date somewhere [sorry I can't find the reference just now] says he's not going to deal with until he's got geometrical shapes disciplined. [Note ** for a wind-up.] Edit: ah, managers with budgets, toll-highways are mentioned in Hugh's TAAMOTI; but I think that's not the earliest place they get considered/only to be postponed; also coloured circles being S-by-E of circles.

I just searched for "auxiliary" in DTATRM and DBE, and found only one (completely unrelated) instance of the word in DBE.

I note that an awful lot of discussion about inheritance misunderstands how it should be used in object oriented programming, which I mention because that's where specialisation-by-extension holds sway. (If that's not at all where you were going with mention of S-by-E, then my apologies.)

The usual object-oriented inheritance examples typically involve peculiar real-world domain taxonomies -- zoo animals and vehicles and the like -- that are nothing like real programming hierarchies.

Yes. Likewise I find the geometrical shapes nothing like programming hierarchies. So I'm sticking to commercial database examples.

In real object-oriented programming, inheritance hierarchies are used to describe computational mechanisms that are hierarchical by levels of abstraction, rather than by contents of data structure.

For example, a typical hierarchy might start with a base class or interface called Report which defines the characteristics of all reports.

Inherited from Report might be SectionedReport, which defines reports with headings and footers and sections.

OK. Auxiliary relvar with headers/footers details. A report not appearing in that auxiliary is a non-Sectioned Report.

Inherited from SectionedReport might be ColumnarReport, which is a report with columns and headings and footers and sections.

OK. Another auxiliary relvar with the column details. Inclusion Dependency that ColumnarReports must be a subset of SectionedReports.

Inherited from ColumnarReport might be TrialBalance, which is an application-specific report with a title heading, blank footer, and account-type sections and account & debit & credit columns with a grand total.

And so on.

And so on. Note this doesn't need TTM's IM; and the TTM texts do say that, but I think they don't say it loud enough or clear enough. So the casual reader is likely to think the TTM's IM machinery is addressing S-by-E "inheritance". Edit: I remember I said on the forum the IM machinery is overkill for S-by-E, and got directed to some section of some text; I can't now find that text, which I think underlines the not loud enough or clear enough.

[To repeat:] (If that's not at all where you were going with mention of S-by-E, then my apologies.)

I was taking S-by-E and auxiliary relvars for granted; and mentioning them merely to get them out of the way.

 

Good object-oriented programming strongly encourages the programmer to then code to the highest level of abstraction possible. In other words, the programmer should reference Report wherever possible and reference TrialBalance as little as possible.

Good object-oriented programming also strongly encourages the programmer to make all subclasses of a superclass substitutable for the superclass. In other words, all subclasses of Report should behave equivalently as a Report. This is the Liskov Substitution Principle.

Done properly, and in general, you code algorithms to abstractions. In other words, you write algorithms to work with base classes or interfaces, then you implement concrete classes that define enough specific functionality to make the algorithms useful.

Sure. So you can wrap the Report relvar in a Report class; and you might wrap Report-join-headers/footers-auxiliary in a SectionedReport class; with class inheritance such that SectionedReport implements the Report interface by reading/writing the Report relvar.

I mention all this only to point out that I'm not sure where relvars of any kind -- auxiliary or otherwise -- fit it into that. In general, object oriented programming -- including (and perhaps in particular) its inheritance hierarchies -- are about structuring code, not data. As such, data-driven S-by-C inheritance is categorically distinct and unrelated to code-driven structural inheritance. Indeed, I would thus expect them to be compatible but not overlapping; usable together or apart as appropriate to solve completely different problems -- one set of problems related to structuring data, another set of problems related to structuring code -- in a hypothetical D.

Yes. The auxiliary relvars mechanism is specifically to serve OO structured code that reads/writes the database. That's orthogonal to whether some of the attributes in the database might want to be constrained to be strictly-positive, be based on a CHAR field of format 'P'nnnn, etc.

Then I'm going to consider S-by-C for arithmetic operations, specifically over Integers, constrained types: POSINT, NONNEGINT.

  • A program could constrain a divisor to be POSINT, thereby using the type system to avoid divide-by-zero.
  • Is this useful? In particular, if the divisor is an expression (á  la RM VSS2) can the type system derive that the result could never be zero?
  • Suppose the divisor expression is a multiplication: it'd require both factors be POSINT, so far so good.
  • Suppose the divisor expression is an addition: it'd require at least one summand to be POSINT, the other could be NONNEGINT, not so good.
  • Suppose the divisor expression is a subtraction: it'd require the minuend be strictly greater than the subtrahend. That's not a type-characteristic of either operand, no good at all.
  • Then suppose the divisor is a subtraction for which the subtrahend is a multiplication: it's fine to produce zero from that multiplication, no need to constrain the factors to be POSINT; this is getting well beyond what type inference can typically cope with.
  • Likewise if we were trying to constrain integer division to always produce an integer result: that's not a type-characteristic of either operand individually.
  • Likewise trying to type-constrain arithmetic operations to avoid arithmetic over/underflow.
  • Etc.

So this is my difficulty with the claim that 'dynamic typing' is a type system: if some language wants to classify divide-by-zero as a type error -- as opposed to just any old run-time exception -- a S-by-C POSINT can't 'reach out' through type-solving to the rest of the program to avoid run-time exceptions. That is, in general: there are some programs it can see would never produce a zero divisor; there are many for which it could only see they might/not produce a zero divisor; and this is not bumping into the constraint-inference is undecidable issue; it can happen with quite easily inferrable constraints.

And isn't this a general limitation on S-by-C? Statically it is not possible to determine that a program will preserve constraints. Then there's always a possibility a (allegedly) well-typed program can still 'go wrong' -- that is, throw a run-time exception. Then classifying that exception as a type-error strikes me as unhelpful playing with semantics.

That is, one of the three-out-of-three: Static type checking we get by shifting the semantics, but not achieving the spirit of 'well-typed programs can't go wrong'.

Then I'm just not seeing the merit of S-by-C. Indeed it would be better if the TTM Selector for POSINT actually executed some code to check its argument was positive. IOW if a Selector were a 'Constructor' by that thrice-accursed definition.

I wonder if S-by-C might be (better) replaced with predicate dispatch. In other words, rather than defining something like:

(I've deleted your code because WordPress has murdered the formatting; and since no that isn't what I mean.)
But that's not what you mean, is it?

 

I expect 'operator despatch' to be despatch by statically-determined type. 'Predicate despatch' seems to mean runtime-value despatch; which I've no particular objection to, but it's not a type system mechanism. Having a syntactically-visible mechanism I suppose might help the compiler see what's going on and help with constraint- or predicate-inference.

There might be merit in validating (and throwing an exception) where an intermediate calculation results in zero, rather than waiting to where it gets assigned to a var, or consumed by a divide operation. Then invoking a Selector to run that validation might be ergonomic. I just don't see that behaviour as part of the type system -- especially where the validation needs comparing two or more results.

So I guess the litmus test is: what are the merits of having distinct types POSINT, NONNEGINT, INT, as opposed to merely some runtime predicate-like/if-then-else/case-despatch mechanism to detect the sign of an INT?

 

Note **: <tongue in cheek> an ellipse is a circle extended with a not-necessarily-distinct second focus; a rectangle is a square extended with a width not necessarily equal to height. So stretched-circles are a subset of circles; stretched-squares are a subset of squares. Are you worried that I've made qualified-X into a non-X? Well are paste-diamonds diamonds or not? Is fool's-gold gold or not? There's a core of attributes common to all; there's auxiliary attributes specific to one variety. </tongue in cheek> Edit: if there's a serious point here to do with subtypes-are-subsets, it is that the subsetting is a consequence of the representation in a data structure; not something intrinsic in the real-world objects being represented.

So this is my difficulty with the claim that 'dynamic typing' is a type system: if some language wants to classify divide-by-zero as a type error -- as opposed to just any old run-time exception -- a S-by-C POSINT can't 'reach out' through type-solving to the rest of the program to avoid run-time exceptions. That is, in general: there are some programs it can see would never produce a zero divisor; there are many for which it could only see they might/not produce a zero divisor; and this is not bumping into the constraint-inference is undecidable issue; it can happen with quite easily inferrable constraints.

And isn't this a general limitation on S-by-C? Statically it is not possible to determine that a program will preserve constraints. Then there's always a possibility a (allegedly) well-typed program can still 'go wrong' -- that is, throw a run-time exception. Then classifying that exception as a type-error strikes me as unhelpful playing with semantics.

That is, one of the three-out-of-three: Static type checking we get by shifting the semantics, but not achieving the spirit of 'well-typed programs can't go wrong'.

Then I'm just not seeing the merit of S-by-C. Indeed it would be better if the TTM Selector for POSINT actually executed some code to check its argument was positive. IOW if a Selector were a 'Constructor' by that thrice-accursed definition.

My reading of RM Pre 23 is that:

  1. the intention is to define a new type as a 'set of values'
  2. this new type takes on the set of values of some existing type, excluding values from that set.

As a new type, it has no operators other than a selector which takes literal arguments (which the compiler can check). Your POSINT is statically safe, precisely because it has no operators other than this.

TTM generally does not expect implicit conversions, so conversion functions are selectors taking an argument of the converted-from type. If you define operators, you make the choice whether to introduce operators that can raise run-time exceptions, or not. They are not type errors.

You may decide to allow INTEGER subtraction, by performing conversions each way. The conversion from INTEGER to POSINT may fail, because the value may be out of range. If you allow this operator, you also have to decide how to handle that failure at runtime. It still isn't a type error.

Andl - A New Database Language - andl.org
Quote from dandl on June 14, 2020, 1:17 am

So this is my difficulty with the claim that 'dynamic typing' is a type system: if some language wants to classify divide-by-zero as a type error -- as opposed to just any old run-time exception -- a S-by-C POSINT can't 'reach out' through type-solving to the rest of the program to avoid run-time exceptions. That is, in general: there are some programs it can see would never produce a zero divisor; there are many for which it could only see they might/not produce a zero divisor; and this is not bumping into the constraint-inference is undecidable issue; it can happen with quite easily inferrable constraints.

And isn't this a general limitation on S-by-C? Statically it is not possible to determine that a program will preserve constraints. Then there's always a possibility a (allegedly) well-typed program can still 'go wrong' -- that is, throw a run-time exception. Then classifying that exception as a type-error strikes me as unhelpful playing with semantics.

That is, one of the three-out-of-three: Static type checking we get by shifting the semantics, but not achieving the spirit of 'well-typed programs can't go wrong'.

Then I'm just not seeing the merit of S-by-C. Indeed it would be better if the TTM Selector for POSINT actually executed some code to check its argument was positive. IOW if a Selector were a 'Constructor' by that thrice-accursed definition.

My reading of RM Pre 23 is that:

  1. the intention is to define a new type as a 'set of values'
  2. this new type takes on the set of values of some existing type, excluding values from that set.

As a new type, it has no operators other than a selector which takes literal arguments ...

No, a Selector can take any expression as argument, not just a literal. (RM Pre 23 doesn't talk about Selectors at all. RM Pre 4. a. 2. merely requires a Selector be able to take a literal argument; not that it takes only literal arguments.)

Then applying POSINT's selector to an expression that (dynamically) evaluates to zero is no different to providing that same expression as a divisor.

... (which the compiler can check). Your POSINT is statically safe, precisely because it has no operators other than this.

TTM generally does not expect implicit conversions, so conversion functions are selectors taking an argument of the converted-from type. If you define operators, you make the choice whether to introduce operators that can raise run-time exceptions, or not. They are not type errors.

You may decide to allow INTEGER subtraction, by performing conversions each way. The conversion from INTEGER to POSINT may fail, because the value may be out of range. If you allow this operator, you also have to decide how to handle that failure at runtime. It still isn't a type error.

Not sure I agree with that characterisation of the IM (because a type that's merely a constrained subset of some based-on type doesn't need 'conversion' in the same way as converting FLOAT to INT or v.v.), but no matter. You haven't explained why POSINT needs to be a type with a name distinct from INT. If all the code (or compiler-generated code) is doing is looking for out-of-range values to raise a runtime exception, there's a variety of ways to do that (Dave suggested predicate overloading). The problem remains that the source of the out-of-range might need comparing multiple operands to multiple operators, not examining/inferring the (scalar) type (or Most Specific Type) of any particular expression.

Quote from AntC on June 14, 2020, 3:09 am
Quote from dandl on June 14, 2020, 1:17 am

So this is my difficulty with the claim that 'dynamic typing' is a type system: if some language wants to classify divide-by-zero as a type error -- as opposed to just any old run-time exception -- a S-by-C POSINT can't 'reach out' through type-solving to the rest of the program to avoid run-time exceptions. That is, in general: there are some programs it can see would never produce a zero divisor; there are many for which it could only see they might/not produce a zero divisor; and this is not bumping into the constraint-inference is undecidable issue; it can happen with quite easily inferrable constraints.

And isn't this a general limitation on S-by-C? Statically it is not possible to determine that a program will preserve constraints. Then there's always a possibility a (allegedly) well-typed program can still 'go wrong' -- that is, throw a run-time exception. Then classifying that exception as a type-error strikes me as unhelpful playing with semantics.

That is, one of the three-out-of-three: Static type checking we get by shifting the semantics, but not achieving the spirit of 'well-typed programs can't go wrong'.

Then I'm just not seeing the merit of S-by-C. Indeed it would be better if the TTM Selector for POSINT actually executed some code to check its argument was positive. IOW if a Selector were a 'Constructor' by that thrice-accursed definition.

My reading of RM Pre 23 is that:

  1. the intention is to define a new type as a 'set of values'
  2. this new type takes on the set of values of some existing type, excluding values from that set.

As a new type, it has no operators other than a selector which takes literal arguments ...

No, a Selector can take any expression as argument, not just a literal. (RM Pre 23 doesn't talk about Selectors at all. RM Pre 4. a. 2. merely requires a Selector be able to take a literal argument; not that it takes only literal arguments.)

Of course, but I think that's in the realms of implementation decisions. Yes, one might well have an operator that took an argument of INTEGER and returned a POSINT and one might call it a selector but (a) that's really just a conversion function from INTEGER to POSINT (b) it can fail, for some values of INTEGER, and the implementor needs to decide what to do about that. The only guaranteed selector is the one for literals, and that cannot fail.

Then applying POSINT's selector to an expression that (dynamically) evaluates to zero is no different to providing that same expression as a divisor.

Sorry, don't understand. The first case is a conversion function from INTEGER zero to POSINT; the second is a divide-by-zero?

... (which the compiler can check). Your POSINT is statically safe, precisely because it has no operators other than this.

TTM generally does not expect implicit conversions, so conversion functions are selectors taking an argument of the converted-from type. If you define operators, you make the choice whether to introduce operators that can raise run-time exceptions, or not. They are not type errors.

You may decide to allow INTEGER subtraction, by performing conversions each way. The conversion from INTEGER to POSINT may fail, because the value may be out of range. If you allow this operator, you also have to decide how to handle that failure at runtime. It still isn't a type error.

Not sure I agree with that characterisation of the IM (because a type that's merely a constrained subset of some based-on type doesn't need 'conversion' in the same way as converting FLOAT to INT or v.v.), but no matter. You haven't explained why POSINT needs to be a type with a name distinct from INT. If all the code (or compiler-generated code) is doing is looking for out-of-range values to raise a runtime exception, there's a variety of ways to do that (Dave suggested predicate overloading). The problem remains that the source of the out-of-range might need comparing multiple operands to multiple operators, not examining/inferring the (scalar) type (or Most Specific Type) of any particular expression.

This is not about the IM, it's about RM Pre 23. And in my view 23a explicitly says that it creates a new type and as such must have a unique name. Mapping a value from one type into another type is type conversion (or coercion). Taking an operator defined for type A and applying it to a type B and getting a result of type A means two lots of conversions.

An example: we have a questionnaire with answers 1 -> 5, meaning totally disagree -> totally agree. The create a type called QRANGE with the set of values 1,2,3,4,5 as per 23b. We do not intend this type to support arithmetic, but we do intend it to be ordered. There are no operations returning a value of this type, it can only be created by literal selector and it is totally type safe.

Andl - A New Database Language - andl.org