Re: array from static predicate on enumerated type

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

On 2021-03-18 02:30, Matt Borchers wrote:
> On Wednesday, March 17, 2021 at 3:41:16 PM UTC-4, Dmitry A. Kazakov wrote:
>> On 2021-03-17 19:44, Matt Borchers wrote:
>>
>>> I understand what you are saying. But, we don't pass CURVED_LETTERS to Count, we pass a value of CURVED_LETTERS to Count.
>> You cannot pass that value. It is type violation as type operations and
>> the values set are different. [Predicate does not create a new type, it
>> only breaks the old one.] So the value must be converted to the expected
>> type (the conversion can be null) or else the operation must be
>> overridden or inherited with type conversion or else be class-wide and
>> then the value must be converted to a class-wide value.
> 
> So what I think I hear you saying is that values of a sub-types with a static predicate are not valid values of the parent without explicit type conversion -- like values of Natural are valid values of Integer without explicit type conversion.

Each natural value has a corresponding integer value and IF the compiler 
uses same representation for both THEN conversion can be identity 
function. The backward conversion is also identity + constraint check.

>>> In my mind, the value should then assumed to be of the type as declared in the parameter to Count -- which is LETTERS in your example. Obviously any value of CURVED_LETTERS is actually a value of LETTERS. This is how Ada treats this case now.

No. A value may have only one type. Ada treats subtypes as same type, 
but the fact is that a subtype is a distinct type if the behavior is 
different, and it is. So a natural value is not an integer value, it 
only has a corresponding integer value. You can ignore that distinction 
almost everywhere but it is still there.

AFAIK, incoming Ada will have arbitrary range integers. Now, if Natural 
were be a constrained subtype of that [and I am almost certain it will 
not be] then the representation of Natural would become an issue.

>> Yes and it is no different to how Ada treats arrays of CURVED_LETTERS
>> right now.
> 
> Given:
> subtype HEX_LETTERS is LETTERS range A..F;
> 
> When I create an array over Natural Ada does not create an array over Integer.  So I would expect that WITHOUT Static_Predicate, Ada would not create an array over the parent enumeration LETTERS when defined on the sub-type HEX_LETTERS.  So, this was my expectation for CURVED_LETTERS with the Static_Predicate before I read the rules.

As I said, ranged subtypes are done more correctly than predicates. 
HEX_LETTERS does not break array abstractions, CURVED_LETTERS do.

>>> To your question, I would say that the compiler treat the argument for A : LETTERS as a member of LETTERS such that A'First = 0 and A'Last = 11 even if a value of CURVED_LETTERS was passed in (as it does now).
>> Then why you expect a different behavior from an array of CURVED_LETTERS?
> 
> 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.

>>> This discussion is helpful as I am now understanding that what I'm thinking is perhaps also equally inconsistent. My current thinking is that I preferred a value of a sub-type to continue to be comparable (with =) to a value of the parent type, but I also wanted it to behave like a full-fledged type when using its attributes.

Derived types inherit operations, comparison is one of such operations. 
It is difficult to break comparison and so long the representation is 
same it is easy to inherit. BUT once you have different representations 
you start to enjoy all combinatorial fruits of multiple dispatch.

>> You cannot have it both ways.
> 
> Of course, and I'm not requesting what my expectations were.  But, I'm still trying to understand why it can't be done because, after all, if a programmer can write it, then a compiler could code-generate it.

It cannot be done mathematically. A subset is not a subtype. Subtype 
here is used in the Liskov's meaning: S is a subtype of T if any 
proposition p true on T holds on S.

Any constraint breaks something (= some proposition become untrue). A 
rational language design is to allow only constraints that would either

- allow static verification of the program at hand [rather than 
universal substitutability, which is not possible]

- allow formulation of weaker contracts that hold, e.g. adding 
Constraint_Error to the contract is such a method.

Range constraints satisfy the above principles, arbitrary predicates do not.

>>> Nevertheless, it still feels like an unfinished feature as it is now.
>> It is not unfinished. It is irreparably broken.
> 
> And this does not make for good advertising for Ada.

Come on, other languages do not bother themselves with whatever 
correctness issues at all.

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