[RFC] constrained indefinite arrays

[jklmnn]

https://github.com/jklmnn/ada-spark-rfcs/blob/static_arrays/considered/definite_unconstrained_arrays.md

[Fabien-Chouteau]

In the Unresolved Questions I would add whether or not we add attributes and operations specific to this kind of arrays. E.g. how do I know the max possible length, or how do I append one element to the array?

   type Index is range 0 .. 32;
   type Static_Array is array (Index range <>) of Integer with
   Constrained;
   Arr : Static_Array := (0, 1, 2, 3);
begin
   pragma Assert (Arr'Length = 4); 
   Arr (Arr'Last + 1) := 4;
   pragma Assert (Arr'Length = 5); 

[jklmnn]

Maybe I didn't write it down clear enough. The Operational Semantics section states:

Operations on that array such appending and slices will trigger the same checks
as they do for indefinite arrays.

Adding an element or checking the max length is not different from the way it is done in indefinite arrays. You can still check for Static_Array'First and Static_Array'Last to get the static boundaries.

Generally there should be no noticeable difference to unconstrained arrays when using a constrained array. The only difference is the storage in memory.

[Fabien-Chouteau]

So you mean:

   type Index is range 0 .. 32;
   type Static_Array is array (Index range <>) of Integer with
   Constrained;
   Arr : Static_Array := (0, 1, 2, 3);
begin
   pragma Assert (Arr'Last = 32); --  Correct?

This seems counter intuitive to me. How do I know how many actual valid elements there are in the array?

[jklmnn]

You have to distinguish between 'Last on the type and on the object. In you case that would be

pragma Assert (Static_Array'Last = 32);
pragma Assert (Arr'Last = 3);

[jklmnn]

I just checked the current behaviour. 'Last cannot be called on an unconstrained array type. So Static_Array'Last would not be allowed. You'd have to use the index type then:

with Ada.Text_IO;

procedure Arr
is
   type Index is range 0 .. 32;
   type Static_Array is array (Index range <>) of Integer;
   Arr : Static_Array := (0, 1, 2, 3);
begin
   Ada.Text_IO.Put_Line ("Index'Last:" & Index'Last'Image);
   Ada.Text_IO.Put_Line ("Arr'Last:" & Arr'Last'Image);
end Arr;

Index'Last: 32
Arr'Last: 3

As I said for the programmer it behaves the exact same way. The only difference is the memory allocation pattern.

[raph-amiard]

I think this warrants adding an attribute ('Capacity or something)

[sttaft]

Capacity is more consistent with the terminology for bounded containers. In any case, "Constrained" is misleading, because the array is not constrained. The term "Definite" would be consistent with ARM terminology, where it means you can declare an object of the type, but that it might still be unconstrained. On the other hand, Capacity is probably easier for typical humans (as opposed to Ada language lawyers) to understand... ;-)

[jklmnn]

I renamed it to Definite Unconstrained Array.

[raph-amiard]

Can you please add a (more thorough) example to your RFC ? Even though it's pretty simple, examples go a long way.

[raph-amiard]

A few more comments:

• WRT. naming, I think it needs to be clear that this feature is part of the same family as the Max_Size for tagged types. It's not really the case so far, so we need to unify the naming somehow
• It feels to me like being able to create singleton arrays rather than types might be explored too. WDYT ?

You say:

Whether the behaviour of arrays with this aspect is different from regular arrays

Clearly the answer is yes. It needs to, because even assigning an aggregate of the wrong size to a regular constrained array will trigger a C_E. As you can see from the internal discussion on W104-022, we will also probably need additional rules since the size of those arrays can change:

type Arr is array (1 .. 32) of Integer with Constrained;

Inst : Arr := (1, 2, 3, 4);

R : Integer renames Arr (4);

Inst := (1, 2);

--  ??? R

[jklmnn]

Clearly the answer is yes. It needs to, because even assigning an aggregate of the wrong size to a regular constrained array will trigger a C_E.

What would prevent us to do the same on a constrained array? Just because it would fit into the allocated memory doesn't mean that it cannot trigger a C_E. The features that are technically possible are a superset of what currently can be done with arrays. Nothing prevents us from saying we want to restrict that feature set to what is currently available.

My question is not intended to test the technical feasibility but rather if we want to have these improved features or not.

It feels to me like being able to create singleton arrays rather than types might be explored too. WDYT ?

What do you mean by that? Anonymous arrays? One intention of this feature is to use these arrays as return types in functions to avoid needing the secondary stack. I don't see how anonymous types would help here.

[raph-amiard]

What would prevent us to do the same on a constrained array? Just because it would fit into the allocated memory doesn't mean that it cannot trigger a C_E. The features that are technically possible are a superset of what currently can be done with arrays. Nothing prevents us from saying we want to restrict that feature set to what is currently available.

I think the answer is that it would make this new feature pretty useless. The whole point of having this is being able to treat this like a box to an array that you can modify, or at the very least set the length freely at initialization.

We also want some consistency with the other features we're going to link it with conceptually, namely Max_Size tagged types, and discriminated records with default values.

[jklmnn]

I think the answer is that it would make this new feature pretty useless. The whole point of having this is being able to treat this like a box to an array that you can modify, or at the very least set the length freely at initialization.

I think we're coming from different assumptions here. The intent of my initial draft was not to treat it like a box but explicitly treat it like a regular array. The usefulness of the feature is solely in its different behavior in terms of runtime support (namely that it doesn't require any secondary stack support).

[jklmnn]

I improved the example and added some clarifications about the behavior. I also renamed it to Definite Unconstrained Arrays.