[feature] Use Constant_Reference instead of Element in Iterable

[clairedross]

Summary

The Iterable aspect is a GNAT specific aspect that provides user defined iteration over containers. Currently it requires First, Next, and Has_Element functions to iterate over the cursors of the container (at least), and an Element function can be added to obtain iteration over the content of the container (for Item of C loop, instead of for Position in Container loop). I would be interesting to allow providing a Constant_Reference function returning an anonymous access-to-constant view of the element instead of the Element function.

As an example, we currently have:

   type List (Capacity : Count_Type) is private
   with
     Iterable                  =>
       (First       => First,
        Next        => Next,
        Has_Element => Has_Element,
        Element     => Element),

   function Element (Container : List; Position : Cursor) return Element_Type;

We could instead allow:

   type List (Capacity : Count_Type) is private
   with
     Iterable                  =>
       (First       => First,
        Next        => Next,
        Has_Element => Has_Element,
        Constant_Reference => Constant_Reference),

   function Constant_Reference (Container : List; Position : Cursor) return not null access constant Element_Type;

A loop:

for E of Container loop
  P (E);
end loop;

Would be equivalent to:

declare
   Position : Cursor := First (Container);
begin
   while Has_Element (Container, Position) loop
      declare
         Ref : constant access constant Element_Type := Constant_Reference (Container, Position);
         E : Element_Type renames Ref.all;
      begin
         P (E);
      end;
      Position := Next (Container, Position);
   end loop;
end;

Motivation

The use of Constant_Reference would avoid copying the element, in particular in quantified expressions where using a while loop is not an alternative (at least for spark).

Caveats and alternatives

A small caveat is that, since E is a renaming and not an object, it would not be possible to use it at certain places, for example inside Global and Depends contracts. It sound minor to me though.

As a follow-up, we could consider having a way to supply a Reference function that would allow direct mutation inside the container. It is notably more complicated to do that in a SPARK-compatible way though, because of aliasing restrictions, so it may be better to keep it as a separate RFC.

[sttaft]

Clearly a Constant_Reference function is opening up the possibility of dangling or erroneous references if the underlying container is updated while the access value still exists. A safer and perhaps more flexible approach might be to implement something like the Ada 2022 "procedural iterator" which uses the "for X of blah loop" syntax, but implements it by calling a compiler-generated loop body, passing the element to the loop-body procedure as a parameter, either IN, or IN-OUT. See:
5.5.3 Procedural Iterators

[clairedross]

For SPARK this is safe, as ownership forbids updates to the observed object (the container) during the scope of the observer (the element). Also note that safety for Iterable wrt tampering is not addressed on purpose. For example, even as it is currently, there is a possibility to deallocate the current element during the loop, or add some so the loop does not terminate. Iterable is simply defined in terms of the equivalent expanded loop.

[tonunaks]

We discussed this issue on the LD meeting last week. We all agreed that the proposal addresses a real problem and that it would be desirable to proceed. Regarding implementation, however, we haven't found a good solution yet. The solution proposed originally for this issue would inevitably open the door for creating dangling pointers (as already pointed out). It is safe for SPARK but weakens the Ada code. @Nikokrock reminded that the possibility of using private functions in the prototype of Iterable has been discussed before. It would solve the issue, but it is wider and more involved than this proposal.

Regarding procedural iterations, the current understanding is that it would break loop optimization. We would replace one performance issue (copying the iterated elements) with another one (unoptimized loops). We agreed that @ronan-d will investigate an idea that might solve the optimisation issue. We continue the discussion when Ronan reports back with the results.

[clairedross]

I am surprised by this dangling pointer issue to be honest. Iterable is syntactic sugar for while loops. Surely it is not less safe than the thing it is syntactic sugar for. In addition, as stated earlier, Iterable was never supposed to introduce safety guarantees wrt tampering. It is lightweight on purpose. Also note that procedural iterators are not in SPARK, so this is not an actual alternative to the proposed enhancement.

[clairedross]

On a similar note, please do not try to make Iterable safer at the cost of complexity, or we will have to introduce another construct for iteration in SPARK. And it would be a shame as Iterable was introduced for iteration in SPARK....

[tonunaks]

@clairedross, we converged on the decision in LD, and then it got pushed to the background for a while. I converted the issue and related discussions to a RFC now. If you check that this is indeed what you proposed, we will put it in the implementation queue.

[clairedross]

Thanks Tonu, it looks good to me