Re: array from static predicate on enumerated type

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2021-03-19 01:10, Matt Borchers wrote:

> I don't think we can blatantly say that subtypes are types in every sense of the meaning.  If they were distinct then there would be no difference between:
> 
> subtype HEX_LETTERS is LETTERS range A..F;
> 
> and
> 
> type HEX_LETTERS is new LETTERS range A..F;

These are two different type operations. The first creates a derived 
type. The second creates a clone of a type.

> when given:
> 
> type LETTERS is ( A, B, C, D, E, F, G, H, I, J, K );
> 
> Please correct me if I am wrong, but I have always thought that the values A through F in the sub-type were the same values of the parent type and are effectively used interchangeably with the corresponding values of the parent type.

There exist a mapping between the values of a derived type and the 
values of the base type. Depending on the properties of this mapping 
(e.g. conjuctive, surjective etc) you may be able to substitute one 
value for another.

... and independently on that the language may allow you to substitute 
regardless the above. This is what you get with CURVED_LETTERS and 
LETTERS. The language allowed you to substitute CURVED_LETTERS for 
LETTERS even when you should not. In glorious FORTRAN-IV you could pass 
INTEGER*8 for REAL*4. Did that make INTEGER*8 a subtype? No, it did 
FORTRAN-IV broken.

> The sub-type simply provides a kind of restricted "view" constraint. That is, the constraint checking used for variables of these types depends on the type "view" of the variable.

Nothing simple. It is elementary to show why natural is not integer. 
Consider the proposition:

    forall x Integer exists -x Integer

It is almost true for Integer (depending on the range, e.g. 2's 
complement usually has one value that cannot be negated). It is almost 
wrong for Natural. A program relying on this property gets broken if you 
substitute Natural for Integer.

> I don't know if I can explain myself very well. 

You confuse set membership with properties of a set as a whole. A set is 
more than the sum of individual elements. Like a type is not a set of 
values it is a set of values + operations defined on them. Taking out or 
adding values breaks operations.

>>> I think you misunderstood me. Given the following,
>>> function L_POS( x : LETTERS ) return NATURAL is (LETTERS'Pos(x));
>>> and
>>> function CL_POS( x : CURVED_LETTERS ) return NATURAL is (CURVED_LETTERS'Pos(x));
>>>
>>> I would have expected the following results:
>>> 1 <= l_pos(B)
>>> 0 <= cl_pos(B)
>>> 4 <= l_pos(E)
>>> exception <= cl_pos(E)
> 
>> That would be a total catastrophe.
> 
> In regards to what L_POS and CL_POS return, I don't understand why that would be a catastrophe.  Those values seem like reasonable answers to what the programmer requested.  This is really the point of this pose and my question in the first place:  What is the reason that there is absolutely no way to implement useful results for 'First, 'Last, etc. with Static_Predicates?  And because of this, what is the best work-around?  And I do feel like this requires a work-around.

You describe overriding of a base type operation ('Pos) in the same 
breath with claiming it is the same type.

> If CURVED_LETTERS with a predicate is not a sub-type, then it should not be declared with a sub-type keyword.  I like the word you used: subset.  It should have been:
> 
> subset CURVED_LETTERS is LETTERS (B,C,D,G,J);

What should that change? Again, the problem is mathematical, not 
linguistic. Wording changes nothing.

1. What is the relation between instances of CURVED_LETTERS and LETTERS?

2. Which operations are inherited from LETTERS = you can use 
CURVED_LETTERS in place of LETTERS?

3. Which inherited operations get overridden?

4. Which operations are exported [*] for CURVED_LETTERS to LETTERS = you 
can use LETTERs in place of CURVED_LETTERS?

5. Which exported operations get overridden?

-----------
* In Ada, "subtype is" imports and exports everything visible, while 
"type is new with" imports (inherits) only primitive and class-wide 
operations.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de