Re: Is this expected behavior or not

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

On Wed, 13 Mar 2013 18:32:01 +0100, Georg Bauhaus wrote:

> On 13.03.13 16:51, Dmitry A. Kazakov wrote:
> 
>> http://en.wikipedia.org/wiki/Abstract_data_type
> 
> Ada subtypes are not ADTs. Which is the point.

And the difference is?

>> Well, well, according to you Ada's Positive has -1 as a value?
> 
> The Ada type of Positive includes -1 as a value.

This is where ARM becomes relevant again:

ARM 3-2(8/2):

"A subtype of a given type is a combination of the type, a constraint on
values of the type, and certain attributes specific to the subtype. The
given type is called the type of the subtype. Similarly, the associated
constraint is called the constraint of the subtype."

and the final blow:

"The set of values of a subtype consists of the values of its type that
satisfy its constraint and any exclusion of the null value. Such values
belong to the subtype."
 
>> 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.
> 
> Type as defined by the LRM; when the discussion is about how
> you dislike what subtypes are, fine.

Where I said I dislike them?

What I said is that Ada subtype is a type-algebraic operation that produces
a new type which properties are described in ARM. There are other type
algebraic operations which produce array, record types, tagged extension,
class-wide types, generic expansions/instantiations etc. They all are used
to construct new *types* from existing ones.

> However, seeing how
> constraints and predicates work in Ada is not easier if
> by some twist of the discussion the explanation becomes one
> of how LSP and proper subsets create a well known problem in
> a hypothetical or otherwise non-Ada language that involves
> two different types, not Ada subtypes.

> Let "subtype" be an Ada subtype, nothing else, and everything
> becomes consistent again. Not necessarily clear, but consistent.
> Maybe confusing, but consistent. Maybe counterintuitive, but
> consistent.

You are welcome to show how problems of substitutability get solved without
these explanations.

'Succ has the problem of substitutability because of these problems. It is
due to multiple inheritance. Pred'Succ inherits some ordered interface from
Integer and from its own problem space. 'Succ is an operation of the
interfaces. These interfaces collide in Prime.

Ada's design choice was in favor of Integer's order: 'Succ (3)=4. But
user's expectation was the order from the problem space 'Succ(3)=5.

Now whatever definitions you take the problem is there. It is not a problem
of definitions.

>> 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.
> 
> Not same what? Need a reference here.

Use any name you want for the corresponding entities. Whatever name you
choose, I am still able to construct a program which semantics would change
when Integer is substituted by Positive.

Positive is not always substitutable for Integer. However you re-write ARM,
that fact is to stay.

>>> The difference only means that different range constraints yield
>>> different programs.
>> 
>> The difference exists. q.e.d.
> 
> You have shown that different constraints on objects of the
> same type yield different programs. But this is not q.e.d.

I shown that objects of Integer and Positive have different properties.

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