Re: Operation can be dispatching in only one type

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

On Tue, 01 Dec 2009 18:52:15 +0100, Georg Bauhaus wrote:

> Dmitry A. Kazakov schrieb:
>> On Tue, 01 Dec 2009 16:02:21 +0100, Georg Bauhaus wrote:
>> 
>>> Dmitry A. Kazakov schrieb:
>>>> On Tue, 01 Dec 2009 13:13:29 +0100, Georg Bauhaus wrote:
>>>>
>>>>> Then we could rely on the language: compilers will detect
>>>>> uninitialized variables provided these do not have a pragma/keyword/...
>>>>> to say that uninitialized is what the programmer wants.
>>>>> Some fancy means to tell the compiler that this variable
>>>>> does indeed have a good first value like pragma Import.
>>>>>
>>>>>    X : [constant] Car; -- default init,
>>>> The error is here!
>>>>>                        -- undefined,
>>>>>                        -- junk bits. Doesn't matter
>>>>>    --  *no* pragma Import (Ada, X);
>>>>>
>>>>> begin
>>>>>
>>>>>    Spare := X.Tire (5); -- would become illegal,
>>>> Not here!
>>> Why?
>> 
>> Because X is illegal right after begin:
>> 
>> IF accessing X is illegal THEN the corresponding operation does not belong
>> to the type of X THEN the type of X is not Car. q.e.d.
> 
> But the implications of this proof are purely formal,
> and not relevant before X is used.

They are relevant to the declaration of X. It cannot be declared of Car, if
it is not.

> There is no way to perform an operation involving X in
> its own declaration.

But it can be used right after the declaration.

> The difference in views would be that your laws say Don't
> create objects that could be used illegally if there
> were uses that can't be there, though, but for formal reasons.
> Whereas Java's ruling says (at compile time) Your program
> cannot be accepted because this object cannot be in
> a legal state here.

No, Java says, that it self failed to prove that this object is in a state
the programmer might want. This is an absolutely informal statement,
because Java cannot have any idea about what the programmer actually
wanted. The only basis for reasoning might be the object type. But that
tells nothing. So Java speculates that the default constructor is somewhat
worse than copy constructor. Why does it so? Did programmer told this the
compiler? No he didn't. Yes, it might be the case, but then why not to
allow the programmer to say exactly this: do not allow default constructors
for this type? I would even make this a default. E.g. if the programmer
does not explicitly allow default constructors they are forbidden. So

   X : T;  -- Is always illegal unless I do some actions

>> (Provided, we are talking about a typed language)
> 
> I think there is more in what you say than what is covered
> by the words "typed language"?

properly typed language! (:-))
 
>> And this one:
>> 
>> procedure Foo (X : in out Car);
>>    ...
>> begin
>>    Foo (X);
>>    Y := X; -- Is this legal?
> 
> Yes, this is legal, because Foo is called with X having been
> assigned a value.

But Foo might read X in its body before updating it. It can leave it
untouched etc.

>> And if Foo were declared as
>> 
>> procedure Foo (X : out Car);
> 
> We'd have roughly the same as this:
> 
>     X : Car;
> begin
>     X := Foo_as_function;  -- now X can be used
> 
> I see no operational problem.  Is there one?

There is one, Foo might leave X unchanged, unless you introduce further
special rules for out parameters. It will be interesting:

begin
   begin
      Foo (X);
   exception
      when Baz =>
           null;
   end;
   Y := X; -- Is this legal?

Ada does not specify what happens with out parameters updated before an
exception gets raised in the body of Foo:

procedure Foo (X : out Car) is
begin
   if HALT (p) then
      raise Baz;  -- Is this legal?
   else
      X := Merzedes;
   end if;
end Foo;

>>>>> Does the phrase "first value" make sense?
>>>> An object shall not have invalid values. All values are valid if the
>>>> language is typed. Enforcing user-defined construction including
>>>> prohibition of certain kinds of construction (e.g. per default constructor)
>>>> is a different story. 
>>> If you feed this to a Java compiler you will see how it is done.
>>> The Java compiler will not accept a reference to a variable's
>>> component when the variable may not have been initialized.
>> 
>> I consider this model wrong. It is better not to introduce inappropriate
>> values rather than trying to catch them later.
> 
> The Java rule works at compile time. No value is introduced at any
> time during compilation.  Nothing to catch.

Of course there is something to catch. The compiler has to do this. So the
question is at which cost, how many false positives and negatives it will
find? How scalable is this feature for more elaborated types?

>> Java does not have
>> constrained types, so I can understand why they go this way.
> 
> Ehm, I don't see the connection here.  Which one is it?
> 
> When I declare
> 
>    X : Some_Type(Some_Constraint);
> begin
>    -- X may need further "initilization", and assigments, since
>    -- Some_Type is an "open minded" type of a varying nature,
>    -- not a fixed value. Its objects accumulate values.

I mean constraints in a wider sense. For example:

   Some_Time (<>)

e.g. a subtype that would require explicit initialization.

>> I also think that forward uninitialized declarations represent bad
>> style, e.g.:
>> 
>> function Foo (...) return Bar is
>>    Result : Bar;
>> begin
>>    ...
>>    if ... then
>>       raise Baz;
>>    end if;
>>    ...
>>    Result := ...;
>>    ...
>>    return Result;
>> end Foo;
>> 
>> I understand the motivation to declare Result uninitialized (because we
>> could leave Foo via an exception), but I don't like this.
> 
> But assigning the first value when declaring X won't help
> when the initialization can raise exceptions.  How could this change?

I don't follow you. My example illustrated a situation where an
uninitialized value might be an advantage, because one possible outcome of
Foo is exception propagation, in which case leaving Result raw could save
some vital nanoseconds of execution time. I don't buy this.

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