Why Generics for Is_Some_And?

Note	Question: Why does Is_Some_And use a generic formal subprogram parameter instead of an access-to-subprogram (function pointer)?

Answer

The implementation uses a generic formal subprogram:

generic
   with function Pred (X : T) return Boolean;
function Is_Some_And (O : Option) return Boolean;

The Alternative: Access-to-Subprogram

In some languages (or non-SPARK Ada), you might expect:

--  NOT what we do:
function Is_Some_And
  (O    : Option;
   Pred : access function (X : T) return Boolean) return Boolean;

Why Generic Formal Subprogram?

1. SPARK Compatibility

Access-to-subprogram types are prohibited in SPARK. The library is SPARK_Mode ⇒ On, so we cannot use function pointers:

--  NOT SPARK-compatible
type Predicate is access function (X : T) return Boolean;

--  SPARK-compatible
generic
   with function Pred (X : T) return Boolean;
function Is_Some_And (O : Option) return Boolean;

2. Static Dispatch = Inlining

With a generic formal, the compiler knows the exact predicate at instantiation time:

function Is_Positive (N : Integer) return Boolean is (N > 0);
function Positive_Check is new Is_Some_And (Pred => Is_Positive);

--  Compiler can inline Is_Positive directly into Positive_Check

With access-to-subprogram, there’s an indirect call at runtime.

3. No Runtime Overhead

Generic instantiation resolves at compile time - zero indirection, zero function pointer overhead. Critical for embedded/safety-critical systems.

4. Provability

SPARK can reason about the behavior of Pred when it’s a known function at compile time. With access-to-subprogram, the prover doesn’t know what function will be called.

Usage Pattern

--  Define your predicate
function Is_Valid_Age (Age : Natural) return Boolean is (Age < 150);

--  Instantiate once
function Has_Valid_Age is new My_Option.Is_Some_And (Pred => Is_Valid_Age);

--  Use repeatedly
if Has_Valid_Age (Person_Age) then ...

Summary

Concern	Access-to-Subprogram	Generic Formal
SPARK	Prohibited	Full support
Inlining	Indirect call	Direct/inlined
Proof	Unknown target	Known at compile time
Overhead	Runtime indirection	Zero
Syntax	Slightly simpler	One-time instantiation

The generic approach is the idiomatic Ada way for SPARK-compatible higher-order functions.

---

Back to Questions & Answers