Re: Reconsidering assignment

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

On Sat, 09 Jun 2007 15:37:53 -0700, Maciej Sobczak wrote:

> On 7 Cze, 11:27, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
> wrote:
> 
>>> Some important foundations.
>>> A type can be unconstrained/constrained. It can be also a subtype of
>>> another type, adding some more constraints.
>>
>> New subtypes can also be obtained through generalization, i.e. by lifting
>> constraints.
> 
> Yes, but then they are not SUBtypes. :-)

subtype /= subset. Especially if you consider Liskov-Wing definitions. They
defines it in terms of substitutability. A more pragmatic definition would
be:

S is a subtype of T in an operation f when S inherits the interface of f.

>> For example, an enumeration type could be extended
> 
> BTW - the fact that I cannot make a subtype by selecting non-
> contiguous subranges of enum values is really disappointing.

That is because you cannot inherit "..", 'Succ and 'Pred. To have
non-contiguous enumerations, you should have them as a base type/interface
first.

>>> For types that have equivalent value-
>>> and constraint- spaces, the rules for parameter passing are as
>>> follows:
>>> 1. "in" formal parameters can get actual parameters that have
>>> constraints matching or stricter
>>> 2. "out" formal parameters can get actual parameters that have
>>> constraints matching or wider
>>> 3. "in out" formal parameters can only get actual parameters that have
>>> matching constraints.
>>
>>> Any violation of these rules leads to potential constraint error that
>>> cannot be prevented at compile-time.
>>
>> This does not work because most of the base type operations will be lost.
>>
>>    function "+" (Left, Right : Integer) return Integer;
>>
>> This cannot be inherited by Positive according to your rules because the
>> result is out.
> 
> Not necessarily. Note that "+" for Integer was there already by pure
> magic and the programmer didn't have to implement it. Why not having
> similar magic for subtypes of Integer?

Again, it is no matter how "+" is implemented, what matters is its
interface = whether "+" is primitive on Integer'Class.

>> which were ambiguous:
>>
>>    X : Integer := 1 + 1;
>>
>> is it Positive'(1)+Positive'(1) or Integer'(1)+Integer'(1)? You will need
>> complex preference rules to resolve this mess.
> 
> It's a compile-time expression with the value 2.
> Not very complex. ;-)

It is complex, because 1 (as any literal) is a function, an overloaded one.
Positive inherits 1 from Integer. It does not 0.

>> The summary of your program is to map constraint [more generally,
>> substitutability] violations onto types. You do this by disallowing
>> operations, and disallowing is static relatively to the type of the
>> operation. Hence to make it work, all constraints have to be static in the
>> type scope. But the string length is not such a constraint.
> 
> It can be checked at the call site.

>>> declare
>>>   S1 : String := "abc";
>>>   S2 : String := "xyz";
>>>   S3 : String := "klmnop";
>>
>> S4 : String := Read_From_File;
> 
> Good point.
> 
>>> begin
>>>   Safe_Swap(S1, S2); -- OK
>>>   Safe_Swap(S1, S3); -- compile-time error
>>>   Safe_Swap(S1, S3(1..3)); -- OK
>>
>> Safe_Swap(S1, S4); -- ?
> 
> Compiler should cowardly refuse it (that's what "conservative" means).

No, this wouldn't be a typed system anymore. S2 and S4 have exactly the
same type. Therefore there cannot be a type error in Safe_Swap (S1, S4) and
no one in (S1, S2). It would be just inconsistent.

Ada has statically constrained types for this. This is how a typed language
works. If you want to distinguish something between legal and an illegal
you need different types. Legality cannot depend on a constraint. You have
to promote the constraint to a new type.

>>> Now - what am I missing? :-)
>>
>> That Constraint_Error is a valid outcome.
> 
> Somehow the "Error" part of the name doesn't go hand in hand with
> "valid outcome". The whole point of having C_E is to signal *invalid*
> outcome and all my speculations are about avoiding it.

Huh, it is like: the whole point of having -1 is to signal an invalid
return code for fread!

As long as a correct program runs, everything it does is valid. This by the
way is the definition of "correct program." Constraint_Error signals
nothing, it is propagated according to the contract of its emitter.

>> The problem is not that "-" of
>> Integer is inherited by Positive.
> 
> Sure. Positive gets its own "-" by the same magic that gifted it to
> Integer in the first place.

And what does the magic say about 0-1?

>> It shall be.
> 
> I'm not sure about this.

About what? You said that Positive gets [own] "-". The implementation is
irrelevant, as always. The fact is -- Positive inherits the interface of
"-" from Integer. It must be this way. It means that Positive is a subtype
of Integer in "-". Then your magic comes into play to deliver positive 0-1.
 
>> Let Swap have no Constraint_Error in the contract, then it cannot be
>> inherited by Positive, because the inheritance will compose it with
>> Integer->Positive, which has Constraint_Error in its contract. So, you'll
>> be forced to either override it or drop inheritance...
> 
> I would drop inheritance.

No need to change anything then:

type Positive is range 1..Integer'Last;

>> or redesign Foo:
>>
>> procedure Foo is
>>    X : Integer := -1;
>>    Y : Positive := 1;
>> begin
>>    Swap (X, Y);
>> exception
>>    when Constraint_Error =>
>>       -- Aha!
>>       ...
>> end Foo;
> 
> My version:
> 
> procedure Foo is
>   X : Integer := -1;
>   Y := Positive := 1;
> begin
>   Safe_Swap(X, Integer'(Y)); -- explicit conversion (*), beware!

That is not a conversion and so illegal for an in out parameter. A
conversion would be:

   Safe_Swap (X, Integer (Y)); -- Legal Ada, works for in out

> (*) Let's assume this conversion works on "references" and doesn't
> create temporaries.

Why? The compiler is free to implement it copy-in, copy-out, the result
will be same. There is no need in referential semantics what that is not
the problem space requirement. Ada's design [rightfully] tires to remove
any differences between by-value and by-reference.

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