Re: Reconsidering assignment

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

On Mon, 11 Jun 2007 02:04:19 -0700, Maciej Sobczak wrote:

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

1. Ada and other languages have subtypes, but to preconditions.

2. Program correctness (if you meant that following Liskov-Wing) has
nothing to do with subtyping. Correctness is a property of a given program.
Subtyping is a relation between types in a program, which occasionally
might be correct or incorrect. They tried to bind them and failed, because
types systems are too weak to express correctness.

But anyway, the domain sets of the types need not to be proper subsets of
each other in any of these two definitions. There might be some mapping
required, but no more than that. Consider Cartesian product, it is LSP
compatible. (Example: Ellipse inheriting x-axis from Circle).

> Lifting constraints doesn't give subtypes.

LSP certainly does. For example, int is a proper LSP subtype of const int.
Adding constraints is much more offending for LSP subtyping than lifting,
because it breaks in-operations, which are more common.

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

Then you should understand why I am arguing against that hard-wired stuff
(which includes assignment) in favor of abstract interfaces (of unordered /
ordered enumerations and whatever else). People designing Ada's
"enumeration class" considered some semantics to be applicable in all
cases. You do same presuming that ":=" has some God-written properties.

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

Yuck, how many languages would you have in one? I don't want it. I want a
small regular predictable language.
 
> Then let's make the constraint part of the type.

In that case you will be unable to write programs where that part could
vary.

One of the great contributions Ada made to typed systems was dynamically
constrained types and generic programming in terms of those types. We need
not to go back to Pascal.

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

but failed to propose a framework for that. Honestly, it is a very complex
problem of how to enforce statically known constraints to be evaluated at
compile time. Once solved, it would immensely simplify the language and the
libraries of. But beware, it might make generics useless! (:-))

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