Re: Reconsidering assignment

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

On 10 Cze, 11:21, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:

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

I don't see how this might imply anything. If f cares about
preconditions on its arguments, then being a subtype means being a
subset (and if f doesn't care about preconditions then there is little
sense in implying any relation between T and S based on f).
Lifting constraints doesn't give subtypes. Supertype is the correct
term here.

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

Yes, this is what I expect:

type Color is (Black, Red, Green, Blue, White);

I don't want any "..", 'Succ nor 'Pred here.

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

No. Compile-time expression is not executed in the universe of
functions overloaded in the program. It can use completely separate
rules - what matters is the result and whether it fits in the given
type.

> >>>   S1 : String := "abc";

> >> S4 : String := Read_From_File;

> >> Safe_Swap(S1, S4); -- ?
>
> > Compiler should cowardly refuse it (that's what "conservative" means).
>
> No, this wouldn't be a typed system anymore.

Then let's make the constraint part of the type.

> S2 and S4 have exactly the
> same type.

Then let's make them different.

> If you want to distinguish something between legal and an illegal
> you need different types. Legality cannot depend on a constraint.

The whole point of my speculations is to elevate constraints to the
level where they could take part in legality resolutions. I hoped it
was clear.

> >>> Now - what am I missing? :-)
>
> >> That Constraint_Error is a valid outcome.

> As long as a correct program runs, everything it does is valid.

For the appropriate definitioin of "runs". :-)

> >> 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's not only "-". You can overflow the upper constraints as well.
This is, I admit, the place where the whole system gets clunky.
It would be insane to expect programmers to write explicit casts (to
satisfy the "innocent code doesn't lie") absolutely everywhere where
the result of the operation can go out of LHS constraints, because
that would basically hit every arithmetic operation, not only
"-" (except for modulo types, which would be the only "pure safe").
SPARK solves this outside of the type system, but that was not the
intention of my experiment.

So, I admit, the common arithmetics is a place where C_E seems to be
necessary as a "valid" outcome. If explicit casts would be used
everywhere to mark the possibility of having C_E, then we might as
well drop the casts and have this possibility implicitly:

A := Positive(B + C);  -- beware C_E, too much typing
X := Y + Z;            -- beware C_E anyway

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