Verification and Metaprogramming

Part V closes with tools that keep functional patterns honest: law checks, property tests, golden snapshots, and derive stubs that will grow into full codegen.

What This Chapter Covers

• testing::proptest — helpers for run_test + Exit in property tests
• law_test! — monad law checks for concrete type constructors
• failure::pretty — multi-line Cause / Exit rendering for failures
• testing::snapshot — golden snapshot builders (GoldenBuilder, assert_golden)
• FreeAp — free applicative over Effect
• id_effect_proc_macro derives — #[derive(Optics)], #[derive(Fsm)] (stubs); #[derive(SchemaParser)] (full codegen in id_effect_parse)

Property tests with Exit

Enable the optional proptest feature when you want strategy helpers:

[dev-dependencies]
id_effect = { version = "3", features = ["proptest"] }
proptest = "1"

Core helpers work without the feature:

#![allow(unused)]
fn main() {
use id_effect::{run_effect, exit_success_value, Exit, succeed};

let exit = run_effect(succeed(42), ());
assert_eq!(exit_success_value(exit), Some(42));
}

With proptest, use success_value and prop_assert_exit_success inside proptest! blocks (see Part IV Property Testing).

Monad law checks

Use law_test! with function items (not closure literals) for f and g:

#![allow(unused)]
fn main() {
use id_effect::law_test;
use id_effect::algebra::monad::option;

fn inc(x: i32) -> Option<i32> { Some(x + 1) }
fn double(x: i32) -> Option<i32> { Some(x * 2) }

law_test! {
  monad option_i32 {
    pure = option::pure,
    flat_map = option::flat_map,
    fa = Some(3),
    a = 7,
    f = inc,
    g = double,
  }
}
}

Pretty failures

pretty_cause renders indented trees; pretty_exit labels success vs failure branches for logs and test output.

Golden snapshots

GoldenBuilder freezes expected strings; assert_golden_effect runs an effect and asserts the snapshot contract.

#![allow(unused)]
fn main() {
use id_effect::{GoldenBuilder, snapshot_effect_map_flat_map, assert_golden_effect};

assert_golden_effect(snapshot_effect_map_flat_map(), ());
GoldenBuilder::new("my_case", "expected").assert_observed("observed");
}

Free applicative

FreeAp collects effectful work as data, then interpret runs it as a concrete Effect:

#![allow(unused)]
fn main() {
use id_effect::{FreeAp, pure, run_test, Exit};

let free = FreeAp::ap2(
  |a: i32, b: i32| a + b,
  FreeAp::lift(pure(2)),
  FreeAp::lift(pure(3)),
);
let exit = run_test(free.interpret(), ());
assert_eq!(exit, Exit::succeed(5));
}

Derive stubs (proc macros)

id_effect_proc_macro ships derives for optics, FSM, and schema parser codegen:

#![allow(unused)]
fn main() {
use id_effect_proc_macro::{Optics, Fsm, SchemaParser};

#[derive(Optics)]
struct Point { x: i32, y: i32 }

#[derive(Fsm)]
enum Light { Red, Green }

#[derive(SchemaParser)]
struct User { name: String }
}

#[derive(Optics)] generates field lenses and enum prisms backed by id_effect_optics. FSM and SchemaParser derives remain stubs until their crates land.