Re: Surprise in array concatenation

[Georg Bauhaus <bauhaus@futureapps.de>]

Dmitry A. Kazakov wrote:

>>Likewise, a computer might surprise us in suggesting that our
>>fine mathematically thought-out program doesn't quite behave exactly
>>as we thought, because of the naughty computer thingy and its
>>quirks.
> 
> 
> You are mixing inadequate and inconsistent models.

The world (our problem domain) *is* inconsistent,
otherwise, if it were consistent, how could we possibly
know what inconsistency is? We can agree on someting.
(As I said, HALT is the limit, I think we cannot even formally
decide, mathematically, whether consistency is consistent.)

A computer, being a real world item, has a good chance of
being whatever it is, there is no complete knowledge of a
computer's consistency. Mathematically consistent programs
can be helpful when the set of preferred consistency rules
is both specified and relates to the program.

>>We have
>> lo, hi: arrays -> I,
>> item: arrays x I -> values

> What about hi >= lo?

No problem, as hi, lo: arrays -> I are just functions.
(These are "minimal" assumptions, really.)

> What about handling Some_Array (Some_Array'First)
> failure?

Same as handling any indexing failure. But different from, and
possibly unrelated to, elaborating the range that is established by
a pair of index values.

> Note that it fails not because there is no A'First, but because
> the index is wrong? How so? It exists, but wrong!

A'First for an empty array isn't wrong at all, it is just a value
from the set of index values.
An array is associated with two particular values from the set
of index values. Then there is a function,
  item: arrays x I -> values,
defined for some (array, index) pairs, undefined for others.

> Then what would you do
> with modular and enumeration types?

Use subtypes. Computers are finite, so are types. So I say what
I want in Ada, another value to mark off the end. Not nice but
practical. (Real types exist inside computers, computed in finite
time. Mathematical types can exist as "infinite" type look-alikes
as in Haskell.)


>>>Better ADT is what Ada needs.
>>
>>Is Ada a Must for you?
> 
> 
> Sure. C++ shortens my life!

Then don't use C++. But there are practical alternatives to
C++ if you can give up some pieces of Ada.

> Like C++? (:-))

Like many.

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

> I don't want the compiler to decide for me whether
> there must be "off" values or not.

The compiler does not force you to use "off" index values,
it forces you to use Ada. When this limit is not o.K., ...


> The concept of array must be consistent
> with index types having no "off" values, like ring buffers.

I see that you like this view, and I see that many programmers and language
designers use indexing with off-bounds index values.

Some languages can do without index manipulation, and with empty sets.
Consider this SETL/2 example:

program automatic_indexes;

        Couples := { ["Frank", "Lisa"],
                     ["Joe", "Nancy"],
                     ["Jack", "John"],
                     ["Jack", "Lisa"] };

        selpuoC := {[x, y]: [y, x] in Couples};


        print("Just the Two of Us: ",
              {[x, y]: y = Couples(x) | #Couples{x} = 1 and #selpuoC{y} = 1});

        for person in { x: x in domain Couples | #Couples{x} = 1}
                   +  { y: y in range  Couples | #selpuoC{y} = 1}
        loop
                print(person, " says, 'One is enough for me!'");
        end loop;

end automatic_indexes;


 [Eiffel solution]

> This is incompatible with modular and enumeration types. It also has a
> distributed overhead. You either will have no by-copy types or will need to
> store NONE where one bit would otherwise be enough. Then making a hash
> function you'll need to explicitly test for NONE etc.

Are you sure you know these things about Eiffel, as opposed to something
that you think must must be the case with Eiffel?


> Sure. And in mathematics there is no problem to write:
> 
>    forall x in X

Like in many programming languages.

> I in A'First..A'Last that A'Range is 1) ordered, 2) has the lower and upper
> bounds, 3) these bounds belong to the array. These assumptions are not
> always required. Moreover, for some arrays they are wrong.

A range with A'Last > A'First is not wrong, I see that you don't
like it. It seems you want to restrict Ada by disallowing
programmers to freely use this widespread idiom for expressing
empty arrays, because it violates your preferences for some
consistency of ordered indexing, right?