Functional Programming Library for Ada 2022

Releases
1

A production-ready Ada 2022 library providing functional programming abstractions for type-safe computation.

Implements Result<T,E>, Option<T>, and Either<L,R> monadic types with 87 composable operations enabling railway-oriented programming, explicit error handling, and optional value management.

Designed for safety-critical, embedded, and high-assurance applications with full SPARK compatibility.

Release Notes

6 Likes
2

Have you plan to add Improvements ideas · Issue #1 · abitofhelp/functional · GitHub

And SPARK support ?

3

What about dysfunctional error handling? :grinning:

[Sorry, could not resist]

3 Likes
4

I don’t need an alire crate to do that myself.

6

:rocket: Version 3.0.0 Released Today! :partying_face:

Functional Crate @ GitHub

Functional Crate @ Alire

4 Likes
7

:rocket: v3.0.0 Released: 100% SPARK Proof Verification! :partying_face:

Functional Crate @ GitHub

Functional Crate @ Alire

Functional Library v3.0.0 - SPARK Proof Verification Complete

The Functional Ada 2022 library v3.0.0 now has 100% SPARK proof verification with zero unproved checks.

Results

Category Count Status
Flow Analysis 40 :white_check_mark: Verified
Runtime Checks 17 :white_check_mark: Proved (CVC5)
Functional Contracts 19 :white_check_mark: Proved (CVC5)
Total 76 0 unproved

What’s Verified

  • Option[T] - 26 operations with postconditions
  • Result[T,E] - 36 operations with postconditions
  • Either[L,R] - 20 operations with postconditions

Guarantees

  • No runtime errors (overflow, range violations)
  • No uninitialized data access
  • All pre/postconditions proven correct
  • Termination proven for all functions

Commands

make spark-check # SPARK legality
make spark-prove # Full proof (–level=2)

SPARK verification uses test instantiations since gnatprove analyzes instantiated generics, not templates.

8 Likes
8

Hey, just wanted to say thank you for all your hard work!

2 Likes
9

Functional v4.0.0 has been released at GitHub and published on Alire. It includes many improvements, but here are my favorites!

New Exception Mapping Packages

  • Functional.Try.Map_To_Result - Declarative exception-to-Result mapping with
    configurable exception→error kind tables. Supports empty mappings (catch-all)
    or specific exception discrimination.

  • Functional.Try.Map_To_Result_With_Param - Parameterized version for actions
    requiring input context (file paths, user IDs, etc.). Supports indefinite types.

New RAII Resource Management

  • Functional.Scoped.Guard_For - Unconditional RAII guard for automatic resource
    cleanup. Calls Release procedure when guard goes out of scope.

  • Functional.Scoped.Conditional_Guard_For - Conditional RAII guard that checks
    Should_Release predicate before calling Release.

Release Notes v4.0.0

Alire

4 Likes