Version: 4.1.0
Date: 2025-12-18
SPDX-License-Identifier: BSD-3-Clause
License File: See the LICENSE file in the project root
Copyright: © 2025 Michael Gardner, A Bit of Help, Inc.
Status: Released

A production-ready Ada 2022 library providing functional programming abstractions for type-safe computation. Implements Result<T,E>, Option<T>, Either<L,R> monadic types, and Scoped RAII guards with 80+ composable operations enabling railway-oriented programming, explicit error handling, optional value management, and automatic resource cleanup.

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

• Preelaborate/Pure categorization on all packages
• Zero heap allocation - Stack-based discriminated records only
• No controlled types in core - No finalization overhead
• No tasking dependencies - Ravenscar profile compatible
• Bounded memory - Fixed-size structures
• No OS dependencies - Pure Ada 2022

• Comprehensive test coverage (90%+ code coverage)
• Zero dependencies - Ada 2022 standard library only
• Comprehensive contracts - Pre/Post conditions throughout
• Cross-platform - POSIX and Windows tested

Status
Scope	All packages (Option, Result, Either, Version) + comprehensive instantiation tests
Mode	gnatprove --mode=prove --level=2 (full proof)
Results	See CHANGELOG for current proof statistics

The entire library is formally verified using SPARK Ada, providing mathematical guarantees of:

• No runtime errors - Division by zero, overflow, range violations
• No uninitialized data - All variables properly initialized before use
• Contract compliance - Pre/postconditions proven correct
• Data flow integrity - No aliasing or information flow violations

make spark-check    # Run SPARK legality verification
make spark-prove    # Run full SPARK proof verification

The Try and Scoped modules use SPARK_Mode => Off because they interact with exception handling and finalization respectively.

Since SPARK only analyzes instantiated generics (not generic templates), the library includes a comprehensive SPARK test suite (test/spark/) that instantiates all generic operations, providing:

• Full operation coverage: All Map, And_Then, Filter, Zip, Flatten, Fold operations instantiated
• Helper function verification: All predicates and transformers formally proven overflow-safe
• High proof rate: See CHANGELOG for current statistics

Add to your alire.toml:

[[depends-on]]
functional = "^4.1.0"

Then build:

alr build

git clone --recurse-submodules https://github.com/abitofhelp/functional.git

# Or if already cloned:
git submodule update --init --recursive

with Functional.Result;

package Int_Result is new Functional.Result (T => Integer, E => Error);

--  Create results
R := Int_Result.Ok (42);                    --  Success
R := Int_Result.New_Error (Parse_Failed);   --  Failure

--  Check and extract
if Int_Result.Is_Ok (R) then
   Process (Int_Result.Value (R));
end if;

--  With default (or use operator syntax: R or 0)
Val := Int_Result.Unwrap_Or (R, 0);

--  Transform (railway-oriented)
function Double is new Int_Result.Map (F => Times_Two);
R := Double (R);  --  Ok(42) -> Ok(84), Error stays Error

See how the Result monad is used in production:

• zoneinfo: Domain.Error.Result
• tzif: Domain.Error.Result

with Functional.Option;

package Int_Option is new Functional.Option (T => Integer);

--  Create options
O := Int_Option.New_Some (42);   --  Has value
O := Int_Option.None;            --  No value

--  With default (or use operator syntax: O or 0)
Age := Int_Option.Unwrap_Or (O, 0);

--  Chain operations
function Parse is new Int_Option.And_Then (F => Try_Parse);
O := Parse (Input);  --  Some -> parse it, None -> stays None

See how the Option monad is used in production:

• zoneinfo: Domain.Types.Option
• tzif: Domain.Types.Option

with Functional.Either;

package Str_Int is new Functional.Either (L => String, R => Integer);

--  Create either
E := Str_Int.Left ("text");    --  Left variant
E := Str_Int.Right (42);       --  Right variant

--  Fold to single value
Result := Str_Int.Fold (E, On_String'Access, On_Integer'Access);

Use Map_To_Result_With_Param (recommended) for declarative exception mapping:

with Functional.Try.Map_To_Result_With_Param;

package Try_Read is new Functional.Try.Map_To_Result_With_Param
  (Error_Kind_Type    => Error_Kind,
   Param_Type         => String,
   Result_Type        => IO_Result.Result,
   Make_Error         => Make_Error,
   Default_Error_Kind => Internal_Error,
   Action             => Read_File_Raw);

Mappings : constant Try_Read.Mapping_Array :=
  [(Name_Error'Identity, Not_Found),
   (Use_Error'Identity,  Permission_Error)];

Result := Try_Read.Run (File_Path, Mappings);

Use Try_To_Option_With_Param for probe operations:

--  Returns None on any exception, then use Unwrap_Or
Exists := Bool_Option.Unwrap_Or (Try_Is_TZif (Path), False);

# Run all tests
make test-all

# Run unit tests only
make test-unit

# Run with coverage
make test-coverage

Results: All tests passing. See CHANGELOG for current counts.

• Cheatsheet - All operations at a glance
• User Guide - Design philosophy, SPARK, embedded, best practices
• Quick Start - Get started in minutes
• SRS - Requirements specification
• SDS - Design specification
• STG - Test guide
• CHANGELOG - Release history

make submodule-init      # After fresh clone
make submodule-update    # Pull latest
make submodule-status    # Check commits

This project follows:

• Ada Agent (~/.claude/agents/ada.md) - Ada 2022 standards
• Functional Agent (~/.claude/agents/functional.md) - Result/Option/Either patterns

This project is not open to external contributions at this time.

This project — including its source code, tests, documentation, and other deliverables — is designed, implemented, and maintained by human developers, with Michael Gardner as the Principal Software Engineer and project lead.

We use AI coding assistants (such as OpenAI GPT models and Anthropic Claude Code) as part of the development workflow to help with:

• drafting and refactoring code and tests,
• exploring design and implementation alternatives,
• generating or refining documentation and examples,
• and performing tedious and error-prone chores.

AI systems are treated as tools, not authors. All changes are reviewed, adapted, and integrated by the human maintainers, who remain fully responsible for the architecture, correctness, and licensing of this project.

Copyright © 2025 Michael Gardner, A Bit of Help, Inc.

Licensed under the BSD-3-Clause License. See LICENSE for details.

Michael Gardner A Bit of Help, Inc. github.com/abitofhelp

Status: Production Ready (v4.1.0)

• Result[T,E] - 30 operations
• Option[T] - 25 operations
• Either[L,R] - 20 operations
• Try module - 6 functions + child packages
• Scoped module - 2 RAII guard packages
• SPARK compatible (see CHANGELOG for proof stats)
• Comprehensive test coverage (see CHANGELOG)
• Zero external dependencies
• Cross-platform (POSIX, Windows)