Subtypes and type invariants in Ada2012

Subtypes and type invariants in Ada2012

[Victor Porton]

I thought that type invariants are designed for subtypes. I mistook!

--
package X is

  type T is tagged private;

  function F(P: T) return Integer;

  subtype S is T with Type_Invariant => F(T) > 10;

private

  type T is tagged
    record
      X: Integer;
    end record;

end;
--

This does not verify:

$ gnatgcc -c -gnat2012 x.ads
x.ads:7:23: aspect "Type_Invariant" only allowed for private type or 
corresponding full view

So, my question: Is it possible to restrict a subtype with something like a 
type invariant?

I want a subtype restricted by an arbitrary condition. Is it possible?

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

Re: Subtypes and type invariants in Ada2012

[J-P. Rosen]

Le 21/08/2017 à 17:38, Victor Porton a écrit :
> I thought that type invariants are designed for subtypes. I mistook!
> [...] 
> So, my question: Is it possible to restrict a subtype with something like a 
> type invariant?
> 
> I want a subtype restricted by an arbitrary condition. Is it possible?
> 

This is rather a subtype predicate.

Type invariants are here to publicize properties of a private type,
otherwise the user knows nothing about it (since it is private!)
-- 
J-P. Rosen
Adalog
2 rue du Docteur Lombard, 92441 Issy-les-Moulineaux CEDEX
Tel: +33 1 45 29 21 52, Fax: +33 1 45 29 25 00
http://www.adalog.fr

Re: Subtypes and type invariants in Ada2012

[Dmitry A. Kazakov]

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.

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

Re: Subtypes and type invariants in Ada2012

[Victor Porton]

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"?

For me the condition Is_Prime added to a subtype of Natural seems quite 
natural. It is quite natural to have a variable which can hold only prime 
numbers. This may appear in some math software.

I would propose to add public subtype invariants (not only private tagged 
type invariants as now) to Ada2020. Anything particular against this?
 
-- 
Victor Porton - http://portonvictor.org

Re: Subtypes and type invariants in Ada2012

[Dmitry A. Kazakov]

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.

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

Re: Subtypes and type invariants in Ada2012

[Victor Porton]

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

Re: Subtypes and type invariants in Ada2012

[Dmitry A. Kazakov]

On 2017-08-21 19:41, Victor Porton wrote:

> 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)?

What should that change?

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

Prime numbers are scalar, at least in mathematics.

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

Prime numbers have range, it is just so that the range with prime bounds 
is not always a subset of Prime. While any integer interval contains all 
intervals with bounds from it. That in turn is related to whether the 
set is closed upon numeric operations. Prime numbers lose these 
operations, so the set of prime numbers is not an abelian group. 
Nevertheless you still can enumerate primes:

    for I in Prime range 1..13 loop -- Runs through 1,2,3,5,7,11,13

> The hardest part here seems to define such operations as
> 
> Prime + Prime return Natural
> 
> Let us discuss it. I think, something can be invented.

OK, but you should explain the goal. In particular why it should be a 
subtype?

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

It must be a type in order to distinguish between co- and 
contra-variance. So subtype in Ada sense looks like a non-starter.

I think that finesses like arbitrary constraints cannot be expressed at 
the types level. A much easier way IMO is to deal with individual values 
and use SPARK in order to prove properties of concrete variables 
formulated as a post-condition.

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