Re: Surprise in array concatenation

[Georg Bauhaus <bauhaus@futureapps.de>]

Dmitry A. Kazakov wrote:

> Inconsistency means that you can derive P and ~P.

It's you who says this, stipulating the universal applicability
of binary logic. How can I justify that I can only derive
P from {}, and not ~P? Because it turns out to be useful.
Not because the derivation works.


> So far, there were no
> evidences that the world doesn't obey logic.

Tons. Starting at those things for which there is no explanation.
But we don't have a proof that the world is (binary) logical.
Wittgestein has made an attempt, but (of course) he had to give
up (shut up, in a sense, using an abbreviation of his own words).

BTW, people can say P now and ~P at another time, and this causes
very little mental stress.



>>We can agree on someting.
>>(As I said, HALT is the limit, I think we cannot even formally
>>decide, mathematically, whether consistency is consistent.)
> 
> 
> You cannot express the sentence above in a formal language. Which does not
> imply its undecidability. Only proper propositions can be decidable or not.

If the world is logical, as you claim, then our sentences
cannot be illogical, thus our sentences must be proper
propositions, thus decidable.


> You better show a case where [mathematically] inconsistent program could be
> usable. [Windows does not count! (:-))]

Inconsistent with what? Empty arrays having A'First > A'Last
are ubiquituous; I understand you find this inconsistent.

>>>>We have
>>>>lo, hi: arrays -> I,

> If hi and lo are just arbitrary values

I said, hi and lo are functions. I didn't say that they are
arbitrary.


> hi and lo are bounds, as such they have definite contracts. They cannot be
> "just" values. Once you formulate the contract, it will be pretty easy to
> show whether it is consistent = no any properly constructed array object
> violates the contract. It is not rocket science, really...

You have to know the contract of 'First etc. I see they can be surprising,
but I don't see a violation of Ada's well working contracts in
'First > 'Last.


>>Use subtypes. Computers are finite, so are types.
> 
> 
> I don't know what a finite type is. You might mean the domain set of a
> type. Then you are wrong, the sets of values of Ada's universal types
> aren't finite.

Ada's types in a real computer program are finite, no matter what.
Any value in an Ada program is finite due to de facto capacity
constraints.

> You can have a type which values comprise an uncountable set
> of any cardinality [I cannot tell for unreachable cardinals, though (:-))]

I very much doubt that any executable program has ever succeeded in
exstablishing a type representing an uncountable set, other than
symbolically, or by turning it into a countable finite thing, by way
of lazy evaluation.

> It is not the same as to be able enumerate all these values in one program!

For any infinite type,
there needs to be an algorithm or a declaration capable of constructing
the values in the type. For infinite types, the algorithms and declarations
don't exist.

> There is no any limitation on how bit patterns are mapped to the type
> values.

A limit on which items can be mapped to bit patterns is storage capacity.
Storage capacity is a worldly item << infinity.


> I can have 0000->Pi, 0001->e, 0010-><whatsoever>.

I did answer this.

>>>What I want is freedom.
>>
>>Then choose not use empty arrays, or test for 'length = 0, or
>>build your own array abstraction, use use Ada.Containers.Vectors,
>>.... or do not use Ada.
> 
> 
> Ah, that's your definition of freedom... (:-))

I won't ask language designers to rebuild their language
just because I prefer a certain, allegedly more consistent,
design of arrays, preferred by some in some algorithms,
not preferred by others.

 Is it so much better to introduce ubiquituous case distinctions
('Length = 0?) in every (sub)array algorithm just because there happens
to be a mathematical property that may be applied to indexes, forcing
A'First > A'Last to be a bad thing?


> It sounds as if the whole language design would collapse if empty arrays
> were constructed otherwise [properly.] Do you really believe in that?

Sure a lot of algorithms will collapse if they have to adopt your
consistency rules. If you dislike Ada's arrays, that's o.K..

If you claim to have found the only true rule stating what kind of arrays
are consistent with the rule and what kind isn't, then this sounds
like the RM has had inconsistent arrays for a number of years now.
Shouldn't there be an article somewhere that points out the erratic
definitions of array bounds in Ada 83, Ada 95, and the upcoming Ada 05?


> Did I say that?

If you insist on A'First <= A'Last, then it sounds like you want
to restrict Ada's attributes.


> The idiom you trying to push for has a clear application area. This area is
> *narrower* than one of the array idiom.

What is "_the_ array idiom"?

The few array types in some languages that I know don't seem to
have a problem with 

  "The Last Ones Shall be First"



> Then with "off"-values or without them, A'Last shall *not* be less than
> A'First.

Should this sentence start with "Thou shalst not do what everyone else
does"?


> Presently the case A'Last < A'First is used to indicate that there
> is no bounds.

That's wrong, in that it just indicates that A'Last < A'First yields
an empty range.

> It is a quite silly way to handle errors. Instead of an
> immediate response you return nonsensical values

What nonsensical values are returned in text like "3 .. 1"?

result := default_value;
for k in 3 .. 1 loop
 result := x(k);
end loop;

How could this be improved using

if x'length = 0 then
  result := default_value;
else
  for k in 3 .. 1 loop
   result := x(k);
  end loop;
end if;