Re: array from static predicate on enumerated type

[Matt Borchers <mattborchers@gmail.com>]

On Wednesday, March 17, 2021 at 4:41:17 PM UTC-4, Shark8 wrote:

> Because it's undefined, and the operations prohibited. 
> You're jumping from "Let's have a continuous function" to "we can define division by zero as something useful." 
> And you can... but not automatically, and when someone brings up the function F(x) = 1/x and says "well, we have to resolve this issue, as the limit to zero comes from negative it becomes -Infinity, but from positive it becomes positive Infinity." 

This sounds like a strawman argument.  You're saying it can't work because it doesn't work.  I have a valid 1 to 1 mapping of values and that is the purest definition of a function.  It is up to the programmer to define what the mapping is.  Static_Predicate is only defining the list of valid inputs (and the order) to whatever I choose my mapping implementation to be.  A programmatic function does not need to be continuous and nor can it be when it is defined on an enumerated type.  The parent enumeration has an order specified in the program text and the sub-type also has an order.

> The same thing is happening here: you're saying that 'pos, 'succ, etc could be defined -- and that's true -- but you're ignoring the underlying problems. 
> Having something like "P : Constant Array (Primes) of Natural;" could indeed be useful, but what would P(12) be? If Primes'Succ(11) = 13, then what is Primes'Pred(2)? [This latter is a good example because in String manipulation, the 0 value is used for indicating things like "not-found", and we absolutely can say SUBTYPE INDEXER IS VALUE'First..INDEX(VALUE, "NOEXIST"); and have it be sensible when INDEXER is the null-range.]

Assuming,
subtype Primes is Natural with Static_Predicate Primes in 2|3|5|7|9|11|13...;
P : Constant Array (Primes) of Natural;

What I would expect is that P(12) would be an illegal access because 12 is not a valid value of Primes thus cannot be an index and a constraint error or out-of-range error would be thrown.  Wouldn't this just involve the compiler to insert "if x not in primes then raise..." if constraint checking is enabled?  Otherwise you have an erroneous program.  Similarly, Primes'Succ(12) is also illegal.  Primes'Pred(2) also illegal because there is no prime before 2 so presumably you have defined your Static_Predicate to enumerate the primes with 2 listed first.  A similar illegal invocation would be a function F defined with an argument for Primes, like "function F( p : Primes ) return Natural is" and you called F(12).

Regards,
Matt