Re: Is this expected behavior or not

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

On Tue, 19 Mar 2013 16:37:30 -0500, Randy Brukardt wrote:

> "Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de> wrote in message 
> news:vawvqtrqgamw$.1gsl8m14dvk4i.dlg@40tude.net...
>> 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.
> 
> If you can't handle recursive definitions, you'll never get very far in 
> programming language design.

Still, the definition you used is broken. Mine is not.

>>>> 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.
> 
> A type *has* a contract. A contract is made up (in part) of types.

1. *Other* types.

2. To have a contract /= be a part of.

>>> 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,"
> 
> No, there is not any equivalence. "Type" is just one property of "Positive", 
> and it might have the same value as that of some other subtype (like 
> "Natural").

The equivalence

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

is that for each Ada-subtype S there exists a corresponding Ada-type T, and
conversely for each T there exists S.

>> 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?
> 
> "The type of Positive" unambigiously identifies that property for 
> "Positive". There is not "name" (that is, identifier) associated with that 
> property.

... and there is no way you could find any difference.

>>> (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.
> 
> Well, if you insist on naming the unnameable, you'll never reach any useful 
> understanding. If you absolutely have to have a name, call it "the type of 
> Positive" or "Positive'Base" (not all types have the 'Base attribute, or you 
> could use that as the name).
> 
> And Positive'Base = Integer'Base = Natural'Base.

But Positive /= Integer /= Natural

Your theory simply does not reflect language facts, thus it is a wrong
theory.

>>> 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.
> 
> "We consider only legal Ada programs" -- please speak for yourself.

Yes, I am a programmer, I am not interested in illegal programs.

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