Re: Reconsidering assignment

[Maciej Sobczak <see.my.homepage@gmail.com>]

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

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

> > 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?
This of course doesn't solve the general problem, because we can have
regular functions as well:

function My_Function(I : Integer) return Integer;

I'm not sure whether it should be inherited by Positive. I would say
no, for the reason of its return type.

> Thus the programmer will have to delegate it:
>
>    function "+" (Left, Right : Positive) return Positive is
>    begin
>       return Positive (Integer (Left) + Integer (Right));
>    end "+";

Not for the magic "+", probably yes for My_Function (and only if
My_Function still makes sense for the subtype - but it's the
programmer who should know; on the other hand, if it doesn't, then
maybe it should not be a subtype).

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

> > procedure Safe_Swap(X, Y : in out String) with X'Length = Y'Length;
>
> This does not change anything, because the constraint is not static.

But can be statically checked at the call site - most likely
conservatively, but nothing more is really needed. You can always
explicitly convert.

> 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).
Add an explicit conversion (or view conversion or whatever other
mechanism that ensures the constraint is correct) and then the
compiler will be your friend.

> Note that Ada addresses this issue. If you wanted the above you should
> simply do the following:
>
> type Three_Character_String is new String (1..3);
> type Six_Character_String is new String (1..6);
>
> Done.

Yes. Lot's of typing.

> If you use String instead, then there must be a reason for.

Of course. The point is that this presumed reason is incompatible with
swapping with statically constrained Strings.
Short version:

declare
  S1 : String := "abc"; -- statically constrained
  S2 : String := Read_From_File; -- statically unknown constraint
begin
  Swap(S1, S2); -- no-no
end;

I find it difficult to imagine a practical situation where it would
make sense.

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

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

> It shall be.

I'm not sure about this.

> I would like to see contracted exceptions.

Java guys failed with this exercise, but I can imagine it in some
other contexts.

> procedure Foo is
>    X : Integer := -1;
>    Y : Positive := 1;
> begin
>    Swap (X, Y); --Illegal
> end Foo;
>
> The contract of Foo does not have Constraint_Error, but Swap has it.

Safe_Swap doesn't. That's my point.
And Safe_Swap will not compile in the above context. That's my point
as well.

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

> 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!
exception
  when Constraint_Error =>
    -- Aha! I was explicitly asking for troubles and I got them
    ...
end Foo;

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

--
Maciej Sobczak
http://www.msobczak.com/