Why doesn't Ada/SPARK have lifetimes?

General
1

Hope this doesn’t sound too dumb, but why doesn’t SPARK have explicit lifetimes like rust does?
Does SPARK just assume what your lifetimes are and proves them for you?

2

In Ada, there are several things that play into this, first:

  1. Local declarations; because Ada allows return-values of complex types, like unconstrained arrays, this tends to alleviate much of the need for accessed (pointers), combined with the modes in, out, in out and the ability to use same unconstrained arrays as parameter-types, this virtually eliminates the need for pointers.
  2. Generic — Because generics can have subprograms and objects (of modes in or in out) you can directly reference [possibly mutably] an item without having to use pointers.
  3. Type lifetimes; likewise (and because nested packages/declare-blocks are useful), we know that an access-type’s existence (and therefore all values of that type) can only be, at most, that of the type it accesses. — Therefore, Ada implementations are given permission to free all accesses whose type goes out of scope.

In short, Ada uses ‘lifetimes’ differently (more type-centric and structural) than you’re thinking (scope of a pointer), and as one programmer likes to say about Ada: “To a first order approximation: you never need access types in Ada.”

3

This maybe?

4

There’s a rationale for this in the paper Recursive Data Structures in SPARK (in the “Related Work” section):

The ownership rules introduced in SPARK are largely inspired by the Rust language [11]. The differences are mostly motivated by the need to comply with the preexisting Ada semantics of pointers. In addition, SPARK was aiming at coming up with a subset as easy to verify as possible. The resulting model is simpler because it does not make lifetime of borrowers explicit, and aliases created through borrows are always statically known.

5

I very much agree with this, but it’s really hard to describe this to people. I use like 1/100th the number of pointer-like things in Ada versus C++ since I don’t have to manually do const T& for “class-likes” (limited or tagged).

Access types aren’t “just” pointers, they also carry their accessibility with them. Overall, Ada has “accessibility rules”, which are a sort of primordial concept of lifetime. An access type is sort of assumed to have the lifetime of the entirely program scope in which it’s visible, if it’s in a package, then it’s lifetime encompasses all places that type is visible. If you point at an object which has a lifetime shorter than that you get a compile-time error and are forced to use 'Unchecked_Access.

Accessibility is… complicated. That part of the spec has a note calling it “The Heart of Darkness.” Not all rules can be checked statically, so sometimes there are runtime checks inserted. :cry:

Ada has (to me) two types of access types: “storage pool”, (i.e. usually heap only) (type T is access Integer) and “anywhere”, heap OR stack (type T is access all Integer). Pointers are also nominally typed, not structurally typed, like in Rust/C/C++. There’s also “access parameters”, but I’m a bit fuzzy in that area and leave it to folks who don’t just write “fun and fluffy Ada” like me.

type Foo is access all Integer;
type Bar is access all Integer;

--  ...

F : Foo := new Integer'(5);
B : Bar := new Integer'(6);
F : Foo := B;  --  COMPILE ERROR

Note also that you cannot point to anything on the stack unless it’s aliased:

Fail : Integer;
OK : aliased Integer;

-- ...

F := Fail'Access;  -- COMPILE ERROR, not aliased
F := OK'Access;   -- OK

This applies also to parameters:

procedure ABC (U : Integer; V : aliased Integer) is
   G : Foo := U'Access;  -- COMPILE ERROR
   H : Foo := V'Access;  -- sort of OK... pretty sure actually need 'Unchecked_Access here because of accessbility rules
begin
   -- ...
end ABC;

This is because things that look like they’re “on the stack” aren’t guaranteed to even have an address! (they could be optimized into a register). You also cannot point to an element of a record unless it’s marked as aliased.

If we want to use a pointer temporarily, we can just do that, and the type doesn’t escape the subprogram:

procedure Another (V : aliased in out Integer) is
    type Int_Ptr is  access all Integer;  -- Int_Ptr type is only visible inside this subprogram
    My_Ptr : Int_Ptr := V'Access; -- OK
begin
   -- ... 
end Another;
6

Access parameters (and access discriminants and components) are explicit references.

An important distinction to the named access type is that an anonymous access parameter can be controlled and therefore you can dispatch on it:

   type T is tagged ...
   procedure Foo (X : access T); -- This is a primitive operation
   function Bar return T;        -- Ditto
7

There is also this video which shows SPARKs borrow checker being used with the added benefit of guaranteeing memory leak prevention. I’ve wanted to use this feature but haven’t actually needed to yet.

8

I’ll be honest, I find that final thought process to be a bit uneasy for me. For simple things sure, but there are a lot of cases where you will want to use a container, which use pointers (disguised as Cursors, but they can dangle, at least in every implementation I’ve seen including GNAT) or some complex things with limited types (for which there could be containers, but ARG doesn’t want to support that).

I agree that Ada discourages the use of access types and provides a lot of really good ways to avoid them (which I love to use), but virtually eliminates is maybe too strong for my taste.

9

Do not use cursors. Use indices:

  for Index in 1..Container.Size loop
     ... Container.Get (Index) ...
  end loop;

P.S. It is very unfortunate that for indexation a model based on explicit references was chosen. It should have been a purely procedural getter/setter pair, primitive only if the container type is tagged.

Yes, however many cases are due to language design issues. E.g. you need access to task only because the finalization model is insufficient. Access discriminants are frequently used because full multiple inheritance is absent. One can consider recursive types for linked lists etc.

But the point to be made is whether the language attempts to decorate pointer or to replace them with higher order constructs. Ada attempts the latter.

10

Definitely for vectors, but for other containers, it is more of a problem. It’s one of the reasons I tend to favor Vectors as a container whenever possible.

11

Two things, (1) he did say first-order approximation, and (2) having a ‘cursor’ does not, in itself, require pointers, for proof: For X in Some_Array'range – the X there is, conceptually, a cursor.

Perhaps it is a bit strongly stated, but I don’t think that it is incorrect or badly-stated; after all, even though there are facilities for manual and semi-manual memory-management, you don’t have to use them very often at all.

Indices are, conceptually, cursors.

12

Cursor is an absolute reference to an element. It is used without the container. And here lies the problem because a cursor may outlive the container. It is link to the container is implicit and not enforceable without considerable overhead.

Index is a relative reference. It cannot be used without the container which gives safety and clarity. On the other hand if the elements are wandering inside the container index may become volatile. Also there is a distinction between index and position/offset which confuses non-Ada users expecting indices to slide as if they were positions.

Ideally we want all absolute references maintained by the language. So [in]out parameter passing mode or renaming of a dereference or iteration (for E in C loop) go. All other cases should be covered by indices.

13

IIRC, this is incorrect: the cursor is bound to the collection.
I’ll think on the other stuff you said, as I’m working on (what I hope) will be a better system for specifying indexability.

14

…or this, in Ada 2022?

   for Item of Container loop
      --  do what you need with Item
   end loop;
15

Does this make copies or use references? I took some incredible hits in septum in high usage containers since I didn’t realize I was making copies (I was silly and used Element() instead of Constant_Reference()).

16

Only logically. If you try to embed that logic into the cursor you will get a heavy, ineffective implementation based on run-time checks, which will lack safety anyway.

The compiler has necessary information, so it must a language construct, but then you do not need a typed cursor object at all. You just use the element name instead and replace operations on cursors by some iteration/traversal schema.

17

Unfortunately it is not done right as it requires tagged container type and helper types. In my view it should be an aspect or whatever definable on any pair of types: Container/Element. E.g. you should be able to

   Octet : Stream_Element;
begin
   for Bit in Octet loop
      ...
   end loop;

P.S. Taggedness by itself were no problem if Ada had external tags for by-copy types. But it has none. Helper types is a mess.

18

If you’re asking about the for X of Iterable..., then ARM 5.5.2(6/3) has this (and more) to say about the Generalized Loop Iteration:

If the loop parameter is a constant (see above), then the indexing uses the default constant indexing function for the type of the iterable container object for the loop; otherwise it uses the default variable indexing function.

It follows from ARM that either the Constant_Indexing or the Variable_Indexing function is used depending on constness of the object, on the “handedness” of the operation (read v. write) and on which of the two aspects are provided.
For Ada.Containers.Vectors these aspects are set to Constant_Reference and Reference, respectively, so Element is not being used. This Godbolt example concurs.

When you write your own container, you choose which of the indexing aspects you want to provide. The compiler will then permit or reject the use of the generalized loop iteration based on that. For example, if you specify Constant_Indexing, but not the Variable_Indexing, the following will happen:

declare
   Var_Cont : My_Own_Container := [1.0, 1.0, 1.0];
begin
   for X of Var_Cont loop
      Ada.Text_IO.Put (X'Image & " ");  --  permitted
      --  X := 0.0;  --  rejected, error: left hand side of assignment must be a variable
   end loop;
end;