Version: 4.1.1
Date: 2026-06-08
SPDX-License-Identifier: BSD-3-Clause
License File: See the LICENSE file in the project root
Copyright: © 2025-2026 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.
| Type | Operations | Purpose |
|---|---|---|
| Result[T,E] | 30 | Success/failure with typed errors |
| Option[T] | 25 | Optional values (presence/absence) |
| Either[L,R] | 20 | Disjoint unions (one of two types) |
| Try | 6 + child packages | Exception-to-functional bridges |
| Scoped | 2 | RAII resource guards |
- 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| Package | SPARK_Mode | Description |
|---|---|---|
Functional.Result | On | Result[T,E] monad (30 operations) |
Functional.Option | On | Option[T] monad (25 operations) |
Functional.Either | On | Either[L,R] type (20 operations) |
Functional.Version | On | Version information |
Functional.Try | Off | Exception boundary (by design) |
Functional.Scoped | Off | RAII guards (requires finalization) |
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 buildgit clone --recurse-submodules https://github.com/abitofhelp/functional.git
# Or if already cloned:
git submodule update --init --recursivewithFunctional.Result;
packageInt_Resultisnew Functional.Result (T => Integer, E => Error);
-- Create results
R := Int_Result.Ok (42); -- Success
R := Int_Result.New_Error (Parse_Failed); -- Failure-- Check and extractif Int_Result.Is_Ok (R) then
Process (Int_Result.Value (R));
endif;
-- With default (or use operator syntax: R or 0)
Val := Int_Result.Unwrap_Or (R, 0);
-- Transform (railway-oriented)functionDoubleisnew Int_Result.Map (F => Times_Two);
R := Double (R); -- Ok(42) -> Ok(84), Error stays ErrorSee how the Result monad is used in production:
withFunctional.Option;
packageInt_Optionisnew 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 operationsfunctionParseisnew Int_Option.And_Then (F => Try_Parse);
O := Parse (Input); -- Some -> parse it, None -> stays NoneSee how the Option monad is used in production:
withFunctional.Either;
packageStr_Intisnew 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:
withFunctional.Try.Map_To_Result_With_Param;
packageTry_Readisnew 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);| Category | Operations |
|---|---|
| Constructors | Ok, New_Error, From_Error |
| Predicates | Is_Ok, Is_Error, Is_Ok_And, Is_Error_And, Is_Ok_Or, Is_Error_Or, Contains |
| Extractors | Value, Error |
| Defaults | Unwrap_Or, Unwrap_Or_With |
| Transforms | Map, Map_Or, Map_Or_Else, And_Then, And_Then_Into, Map_Error, Bimap, Zip_With, Flatten, To_Option |
| Recovery | Fallback, Fallback_With, Recover, Recover_With |
| Validation | Ensure, With_Context |
| Side Effects | Tap, Tap_Ok, Tap_Error |
| Operators | "or" (Unwrap_Or, Fallback), "=" (Contains) |
| Category | Operations |
|---|---|
| Constructors | New_Some, None |
| Predicates | Is_Some, Is_None, Is_Some_And, Is_None_Or, Contains |
| Extractors | Value |
| Defaults | Unwrap_Or, Unwrap_Or_With |
| Transforms | Map, Map_Or, Map_Or_Else, And_Then, Filter, Zip_With, Flatten |
| Fallback | Or_Else, Or_Else_With, Fallback |
| Side Effects | Tap |
| Conversion | Ok_Or, Ok_Or_Else |
| Operators | "or", "and", "xor", "=" |
| Category | Operations |
|---|---|
| Constructors | Left, Right |
| Predicates | Is_Left, Is_Right, Is_Left_And, Is_Right_And, Is_Left_Or, Is_Right_Or, Contains |
| Extractors | Left_Value, Right_Value, Get_Or_Else |
| Transforms | Map, Map_Left, Map_Right, Bimap, Swap, And_Then |
| Reduction | Fold, Merge |
| Conversion | To_Option, To_Result |
| Operators | "=" (Contains) |
| Function | Purpose |
|---|---|
Try_To_Functional_Option | Convenience for Functional.Option |
Try_To_Option_With_Param | Parameterized Option bridge |
Map_To_Result | Declarative exception mapping tables |
Map_To_Result_With_Param | Parameterized declarative mapping |
Try_To_Result | General bridge (deprecated) |
Try_To_Functional_Result | Convenience for Functional.Result (deprecated) |
| Package | Purpose |
|---|---|
Guard_For | Unconditional RAII guard for automatic cleanup |
Conditional_Guard_For | Conditional RAII guard with Should_Release check |
# Run all tests
make test-all
# Run unit tests only
make test-unit
# Run with coverage
make test-coverageResults: 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 commitsThis 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.1)
- 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)