Re: Subtypes and type invariants in Ada2012

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

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