Re: Subtypes and type invariants in Ada2012

[Victor Porton <porton@narod.ru>]

Dmitry A. Kazakov wrote:

> On 2017-08-21 18:29, Victor Porton wrote:
>> Dmitry A. Kazakov wrote:
>> 
>>> On 2017-08-21 17:38, Victor Porton wrote:
>>>
>>>> So, my question: Is it possible to restrict a subtype with something
>>>> like a type invariant?
>>>
>>> Type invariant is not a restriction of public interface/properties, it
>>> is an implementation detail. So it should never produce a [sub]type.
>>>
>>>> I want a subtype restricted by an arbitrary condition. Is it possible?
>>>
>>> Arbitrary condition breaks type operations. E.g. condition Is_Prime (X)
>>> breaks more or less everything (assuming covariance). All restrictions
>>> do. A few don't break much, e.g. range constraints.
>> 
>> I don't get. What do you mean saying "breaks"?
> 
>     Prime + Prime not in Prime
> 
> Properties of the set of prime numbers are not ones of the set of
> integer numbers.
> 
>> For me the condition Is_Prime added to a subtype of Natural seems quite
>> natural.
> 
> The new set loses properties of Natural.
> 
>     Natural + 1 in Natural
> 
> is false for Prime.
> 
>> It is quite natural to have a variable which can hold only prime
>> numbers. This may appear in some math software.
> 
> Subtyping is not about individual values it is about sets of values as a
> whole. Properties of prime numbers require a new type with other
> operations. E.g.
> 
>     Prime + Prime return Natural (contra-variant)
> 
> Then
> 
>     X : Prime := 13;
>     Y : Prime := X + 1; -- Type error (not a subtype!)
>     Z : Natural := X + 1; -- OK
> 
>> I would propose to add public subtype invariants (not only private tagged
>> type invariants as now) to Ada2020. Anything particular against this?
> 
> It would not make sense.

Maybe it makes sense to allow subtype predicates, but make the subtype with 
a predicate no more a scalar (even if its base is a scalar)?

We could define "prescalars". Prime numbers would be an example of 
prescalars.

Prescalars would have some but not all properties of scalars. For example 
prescalars would have base range but no range.

The hardest part here seems to define such operations as

Prime + Prime return Natural

Let us discuss it. I think, something can be invented.

For example, the operations returning the base type of a prescalar could be 
automatically defined.

-- 
Victor Porton - http://portonvictor.org