search

AdaCore / ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
63 stars 28 forks source link

[RFC] Fixed array lower bound #38

Closed QuentinOchem closed 4 years ago

QuentinOchem commented 4 years ago

This is an initial proposal allowing to fix the lower bound of an array type, in an attempt at fixing some Ada-specific performance footprint.

Link to text: https://github.com/QuentinOchem/ada-spark-rfcs/blob/master/considered/rfc-lower-bound.rst

kanigsson commented 4 years ago

There are in fact two ways (I know of) to force a fixed lower bound:

   type My_String is array (Integer range <>) of Character;

   type String_Based_Zero (Len : Integer) is record
      Data : My_String (0 .. Len);
   end record;

and

   type My_String is array (Integer range <>) of Character
   with Predicate => My_String'First = 0;

Maybe the compiler could be made smarter to optimize code in both cases. I think your proposed change is very heavy in comparison to the expected performance gain.

jere-software commented 4 years ago

There are things to consider here though:

type My_String is array (Integer range <>) of Character;

type String_Based_Zero (Len : Integer) is record Data : My_String (0 .. Len); end record;


I do this one a lot, but I will say this is one of the few cases where I feel like Ada pushes me into a bad or unfortunate design.  I'm not using a record because my software problem is better solved by a record.  I'm using a record because Ada can't do this any better way.  This adds noise to my designs and makes it harder to understand for the average and novice reader (I've experienced trying to explain what this is first hand).

type My_String is array (Integer range <>) of Character with Predicate => My_String'First = 0;



I would like this if the compiler could enforce it statically when possible (and ideally without assertions enabled), but this appears to be a dynamic only predicate, which is unfortunate.  But that means Ada would need better compile-time support defined in the language spec.  Sure a compiler vendor could do it themselves, but not being able to rely on the languages rules for stuff like is an awful place to be.  One of the best things C++ did (at least for the embedded landscape) was the constexpr rules.  It gave a specific set of rules for when things "must" be evaluated at compile time by the compiler but the flexibility to let the same code be used dynamically if the inputs were not compile-time.
QuentinOchem commented 4 years ago

There are in fact two ways (I know of) to force a fixed lower bound:

   type My_String is array (Integer range <>) of Character;

   type String_Based_Zero (Len : Integer) is record
      Data : My_String (0 .. Len);
   end record;

This one is actually slightly misleading as Len is really the Last element of the array, not its length. But yes, and documented in the proposal.

and

   type My_String is array (Integer range <>) of Character
   with Predicate => My_String'First = 0;

Maybe the compiler could be made smarter to optimize code in both cases. I think your proposed change is very heavy in comparison to the expected performance gain.

I think this one will open a whole bunch of difficult questions. What if you want more than this condition in the predicate? Do you have another predicate? Overall, I would argue that relying of arbitrary predicate analysis for structural decision is a bit weak.

sttaft commented 4 years ago

An existing Ada 202X AI, on hold, has a related proposal:

http://www.ada-auth.org/cgi-bin/cvsweb.cgi/ai12s/ai12-0246-1.txt?rev=1.3

-Tuck

On Fri, Feb 28, 2020 at 9:29 PM QuentinOchem notifications@github.com wrote:

This is an initial proposal allowing to fix the lower bound of an array type, in an attempt at fixing some Ada-specific performance footprint.

You can view, comment on, or merge this pull request online at:

https://github.com/AdaCore/ada-spark-rfcs/pull/38 Commit Summary

  • Initial proposal

File Changes

Patch Links:

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/38?email_source=notifications&email_token=AANZ4FJ7ODSJ2BEPLJ54J6TRFFX3JA5CNFSM4K535R2KYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IRHDLIQ, or unsubscribe https://github.com/notifications/unsubscribe-auth/AANZ4FMMPEHBCSK5TRVIB3DRFFX3JANCNFSM4K535R2A .