Re: Is this expected behavior or not

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

On Wed, 13 Mar 2013 15:34:41 +0100, Georg Bauhaus wrote:

> On 13.03.13 14:31, Dmitry A. Kazakov wrote:
>> On Wed, 13 Mar 2013 10:45:54 +0100, J-P. Rosen wrote:
>> 
>>> Le 13/03/2013 09:49, Dmitry A. Kazakov a �crit :
>>>>  In Ada subtype
>>>> (here subtype is Ada-subtype) operations are inherited per composition with
>>>> conversion to the base type which is null for in-arguments and sometimes
>>>> range-check of outs (not always, though). E.g.
>>>>
>>>>    F (X : S) = F (S'Base (X))
>>>>
>>>> S is a subtype *because* it inherits F.
>>>
>>> Not at all. In Ada, a type is a set of values.
>> 
>> A type is a set of values bound by operations defined on them. It is
>> values+operations.
> 
> The LRM does not define what it means for sets of values being
> "bound by operations". It does define subtypes and types.

LRM is irrelevant here. See

http://en.wikipedia.org/wiki/Abstract_data_type

>> Even under your (wrong) definition Positive is still different from Integer
>> because Positive does not have values like -1.
> 
> I don't think this is true.

Well, well, according to you Ada's Positive has -1 as a value?

>> Ada subtypes are proper types
> 
> External observations inspired by whichever type theory do
> not apply when judging things from the Ada perspective.

How a type theory may not apply to a programming language? Anyway if you
don't like the theory X, you should propose another theory.

But whichever theory you take, it cannot be consistent with Integer and
Positive being same type, while considering Ada typed.

Ada is typed. Integer and Positive are not same.

>> E.g. these two programs are not equivalent:
>> 
>>    X : Integer := -1;
> ...
>> You cannot replace Integer with Positive without changing the semantics of
>> any possible program, hence they are different.
> 
> The difference only means that different range constraints yield
> different programs.

The difference exists. q.e.d.

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