Re: Is this expected behavior or not

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

On Mon, 18 Mar 2013 17:36:31 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:hiybjkhz3p5d.1x6dxfr1ptgcg.dlg@40tude.net...

>> 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.

See, you just defined a contract in terms of types while using contracts to
define type as same/different/non-existent. You cannot have it in both
ways.

>> 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).

*if* you want to contract a type, *then* that cannot be a part of.

In any case, contract is much less a language term than type. It is more
about design and the problem space. It may apply to a type when the type is
used to represent some domain entity but it cannot define what types are. A
type is values+operations.

> Two operations with different profiles are different, even if 
> everything else is the same (the implementation, names of things, etc.)

Ada has *nominal* equivalence of operations. Two operations are different
just because they are declared in different places. It is not because of
their profiles. On top of that there are rules about overloading/overriding
where profiles get involved, but that is not like C where you can repeat
declarations.

>> 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.

Since there is an equivalence between Positive and the type is "has,"
Positive as a name unambiguously refers to that type, i.e. "Positive" is
the name of the type. Unless you have other legal name for it. But you
don't in Ada. You have absolutely no language means whatsoever to
distinguish Positive and the type of. So, what merits has this distinction
if it cannot be observed?

> (All types in Ada are anonymous.)

Great, then let them be, where there belong to, in the celestial spheres,
and let us call type something that indeed exists in the language and has a
name.

> Types are only about static semantics 
> (that is, compile-time behavior). Run-time semantics aren't involved.

Run-time semantics is what makes program working or not working. Types are
all about run-time semantics nothing else counts.

Type checks is a way to prove something about [run-time] semantics at
compile time. Types neither ensure nor required for a program to behave
correctly. They are a tool to ease reaching that goal.

> 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.

Legality is irrelevant as we consider only legal Ada programs. There exist
legal Ada programs which change their run-time behavior when 'Positive' is
replaced by 'Integer' and reverse.
 
-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de