Re: Is this expected behavior or not

["Randy Brukardt" <randy@rrsoftware.com>]

"Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
news:hiybjkhz3p5d.1x6dxfr1ptgcg.dlg@40tude.net...
> On Fri, 15 Mar 2013 16:17:11 -0500, Randy Brukardt wrote:
>
>> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message
>> news:ewe0v3ck1xdo$.e8rtuof27ke6$.dlg@40tude.net...
>>> On Thu, 14 Mar 2013 17:12:28 -0500, Randy Brukardt wrote:
>>>
>>>> There are some differences in *dynamic* behavior, but that has nothing 
>>>> to do
>>>> with the available values and operations. (The text you quoted from the 
>>>> RM
>>>> about values "belonging" to a subtype is defining dynamic behavior.) I
>>>> recall some Dmitry guy telling us that dynamic behavior is different 
>>>> from
>>>> static behavior, and even claiming that dynamic behavior cannot 
>>>> constitute a
>>>> contract. So it if is not a *contract*, how come it matters for a 
>>>> *type*
>>>> (which is an integral part of describing a contract)?
>>>
>>> I don't understand the point you are making. You cannot derive contract
>>> from behavior, simply because it is converse: contract is imposed to
>>> restrain possible behaviors.
>>>
>>> You might claim that implied contracts of Integer and Positive are 
>>> exactly
>>> same. I doubt that many would agree with that.
>>
>> I certainly wouldn't, because *I* consider the dynamic behavior to be 
>> part
>> of the contract. But, clearly, you don't (and you've indicated that above
>> again. So yes, given your world view, the contracts of Integer and 
>> Positive
>> are exactly the same. That's clear, because they're interchangable in 
>> terms
>> of legality and resolution (anything having to do with compile-time
>> checking). The quote above says that you disagree with yourself. :-)
>
> That would be a consequence of considering them same type. I already said,
> that this a path towards weak typing.
>
> But I don't see where I disagree with myself. Contract /= type. You can
> have same contract and different types. What about:
>
>   type Same is new Integer;

This definitely has a different contract, as it is not compatible with 
Integer's contract. Yes, it has the same set of values and operations with 
the same name, profile, and bodies, but it's still a different contract 
because the types involved are an intergral part of the contract.

> You also can have different contracts put on the same type in different
> contexts. You can have contracts on something that does not involve types
> at all. Anyway, I fail to see how contracts are relevant here.

Because types are an important part of a contract (that is, in Ada terms, 
the profile). Two operations with different profiles are different, even if 
everything else is the same (the implementation, names of things, etc.)

...
> I don't see why. How *any* contract could make something like Positive a
> non-type? There is not many possibilities:
>
> A. Positive is not a type. This is what Georg says. I have no idea what
> this is supposed to mean. That 123 is not Positive, or that "+" is not
> applied to positives? He escapes into some kind of vague philosophy each
> time I ask.

I agree with Georg; Positive is not a type; it *has* a type. Neither is 
Integer a type; it *has* a type. (All types in Ada are anonymous.) As such, 
the "+" that applied to Positive is the same one that's applied to Integer. 
That's *not* the case for a type like the one associated with Same, as you 
declared it above.

> B. Positive is a type. The type is Integer. So Positive = Integer. This is
> evidently wrong because there exist programs which semantics sufficiently
> change when 'Integer' is replaced by 'Positive'. If the language treats
> them same, worse to the language. Luckily Ada checks if Positive is indeed
> positive (well, not always, but almost).

This is also true, except for the first sentence. But you're confusing the 
issue by talking about "semantics". Types are only about static semantics 
(that is, compile-time behavior). Run-time semantics aren't involved. It's 
the same as for profiles, operations, and the like.

In this sense, a type is part of your model for contracts, where there is no 
run-time component.

Run-time semantics get added on top of that, but that has no effect on the 
legality of a program, so it is completely orthogonal to the type/profile.

> C. not (A or B) = my point.

Actually, both A and B are true, claiming their exclusive doesn't make any 
sense. Or maybe it's better to call them irrelevant, as the relationship 
"is" doesn't apply to "Positive" and "type" in Ada (or any named entity, for 
that matter). It would be like saying:

A. Dump truck is not an engine.
B. Dump truck is an engine.
C. not (A or B).

C is the only statement that makes sense here, as a dump truck "has" an 
engine, but it surely is not an engine. (It has many other parts as well, 
and the same is true for Positive.)

                                 Randy.