Re: Is this expected behavior or not

[Georg Bauhaus <rm.dash-bauhaus@futureapps.de>]

On 14.03.13 12:18, Dmitry A. Kazakov wrote:
> On Wed, 13 Mar 2013 22:37:49 +0100, Georg Bauhaus wrote:
> 
>> On 13.03.13 20:28, Dmitry A. Kazakov wrote:
>>
>>>> Ada subtypes are not ADTs. Which is the point.
>>>
>>> And the difference is?
>>
>> Several:
>> Incomparable.
>> In Ada, ADT is not defined.
> 
> How exactly Ada's Positive is not an abstract data type?

Because ADTs are constructs of human mapping from a model space to the
space of language constructs. In this case the latter is defined in Ada
terms. The human's mapping activity causes the---legitimate---
problem with subtype constraints.

> We don't talk about Positive'Base. We do about Positive.

Positive'Succ does *not* declare parameters whose subtype is Positive.
This fact answers most of the other comments, I should think.

For a start, LRM 3.5 again,

22    S'Succ  S'Succ denotes a function with the following specification:

            23    function S'Succ(Arg : S'Base)
                    return S'Base

We don't talk about Positive'Base, you say?

>>    subtype V is Integer range -2 .. +34;
>>
>> does not declare a new type (LRM 3.2.2(1)).
> 
> Nevertheless
> 
>    Positive'Base /= Positive
> 
> and both are types.

The second claim is not true in Ada as relevant to this discussion,
because Positive's subtype constraint does not introduce a type.

>>>  It is not a problem of definitions.
>>
>> Is it *solely* a problem of definitions from the non-Ada world.
> 
> So, it is prime numbers which are broken. Good to know... 

Prime numbers are not defined in Ada, so the definition of Ada cannot
break them. The subtype named Prime that was given was essentially a
constraining predicate. If anyone thinks that 'Succ can be
re-interpreted to refer to a non-interval subset of integral numbers
of an Ada type, and it can't, then that's the problem: A plausible
assumption about the definition vs the actual definition.

>>> I shown that objects of Integer and Positive have different properties.
>>
>> The difference is entirely a consequence of different constraints on the
>> same type that Integer and Positive share.
> 
> Irrelevant. The difference is here. Period.

It is proof that Ada subtypes (not Ada types) and LSP (plus, in this
case, a re-interpretation of 'Succ based on incorrect premises) causes
problems with constraints (not types). The compiler does not reject
  x : Positive := -1,
so there is no Ada typing problem.

There are two problems instead:

1) to think that a subtype creates a type

2) to assume that 'Succ is not what it is