deep_causality_haft 0.4.3

/*
 * SPDX-License-Identifier: MIT
 * Copyright (c) 2023 - 2026. The DeepCausality Authors and Contributors. All Rights Reserved.
 */

//! # The reified free Arrow — `ArrowTerm`
//!
//! The [`Arrow`](crate::Arrow) combinators ([`Compose`](crate::Compose),
//! [`Split`](crate::Split), …) reify the strong category at the **type level**: a pipeline is a
//! nested generic type the caller never names (the finally-tagless / defunctionalized encoding, see
//! [`arrow`](crate::arrow)). That form is executable but not **inspectable, storable, or
//! rewritable** — the term lives only in the type system.
//!
//! [`ArrowTerm`] is the **value-level** reification: the *free arrow* over a generator set `G`,
//! i.e. the initial strong category whose morphisms are freely generated by the elements of `G`
//! under `id`, `compose`, `first`, `second`, `split`, and `fanout`. A term is first-order data
//! ([`ArrowCore`]) that can be pattern-matched, transformed, and interpreted into *any* target.
//!
//! ## Typed construction, erased storage
//!
//! Rust has no GADTs, so a single **storable** term type and **static** `In`/`Out` object types are
//! mutually exclusive: erasing the objects into one enum discards them; keeping them makes the enum
//! variants disjoint types that cannot share a `Box`. The resolution here is *typed construction,
//! erased storage*:
//!
//! - [`ArrowTerm<In, Out, G>`] is a **thin typed façade** carrying phantom `In`/`Out`. Its
//!   builder methods only line up when the wiring is sound, so a mistyped graph is **well-typed by
//!   construction at build time** — it fails to compile (see the `compile_fail` doctest below), no
//!   runtime tag check.
//! - Each method lowers into [`ArrowCore<G>`], the **erased core**: an untyped tree stored with
//!   `alloc::boxed::Box` (no `dyn`, no `unsafe`, no macros), interpreted by
//!   [`ArrowCore::interpret`].
//!
//! ## Interpretation and the universal property
//!
//! Because the core is untyped, interpretation runs over one uniform value universe,
//! [`ArrowVal`] — a binary tree whose leaves carry the payload and whose `Pair` nodes model the
//! monoidal product that `split`/`first`/`fanout` act on. Given an interpretation of the
//! **generators** into leaf endomorphisms, [`ArrowCore::interpret`] extends it *homomorphically*
//! over the whole term: `Compose` sequences, `Split`/`First`/`Second` act componentwise, `Fanout`
//! copies. This is the free arrow's universal property — the extension is **determined entirely by
//! the generators**. Machine-checked in `lean/DeepCausalityFormal/Haft/ArrowTerm.lean`
//! (`haft.arrow_term.interpret_sound`, `haft.arrow_term.free`) and witnessed in
//! `deep_causality_haft/tests/formalization_lean/arrow_term_tests.rs`.
//!
//! The one-way interpreter that lands a term in the Kleisli category of an effect monad
//! (`ArrowTerm → Kleisli<M>`) is built on this in `interpreter` (H4).
//!
//! ```
//! use deep_causality_haft::{ArrowTerm, ArrowVal};
//!
//! // A generator set: two named integer operations.
//! #[derive(Clone)]
//! enum Op { Inc, Double }
//!
//! // Build `first(inc) >>> split(double, id)`, well-typed on pairs by construction.
//! let term = ArrowTerm::<i64, i64, Op>::generator(Op::Inc)
//!     .first::<i64>()
//!     .compose(ArrowTerm::<i64, i64, Op>::generator(Op::Double).split(ArrowTerm::id()));
//!
//! // Interpret the generators into leaf endomorphisms; the term extends uniquely.
//! let interp = |op: &Op, x: i64| match op {
//!     Op::Inc => x + 1,
//!     Op::Double => x * 2,
//! };
//! let out = term
//!     .core()
//!     .interpret(&interp, ArrowVal::pair(ArrowVal::Leaf(10), ArrowVal::Leaf(7)));
//! // (10 -> inc -> 11 -> double -> 22 ; 7 -> id -> 7)
//! assert_eq!(out, ArrowVal::pair(ArrowVal::Leaf(22), ArrowVal::Leaf(7)));
//! ```
//!
//! Mistyped wiring is rejected at build time — the output of the first term is a pair, so it cannot
//! be composed with a scalar-input term:
//!
//! ```compile_fail
//! use deep_causality_haft::ArrowTerm;
//! #[derive(Clone)]
//! struct Op;
//! let paired = ArrowTerm::<i64, i64, Op>::generator(Op).first::<i64>(); // Out = (i64, i64)
//! let scalar = ArrowTerm::<i64, i64, Op>::generator(Op);                // In  = i64
//! // Out = (i64, i64) ≠ In = i64 — the middle objects do not line up.
//! let _bad = paired.compose(scalar);
//! ```

use alloc::boxed::Box;
use core::marker::PhantomData;

/// The value universe interpreted terms flow through: a binary tree with payload leaves.
///
/// Because [`ArrowCore`] erases the object types, interpretation runs over this single uniform
/// universe. `Leaf` carries a payload of type `V`; `Pair` is the monoidal product that `split`,
/// `first`, `second`, and `fanout` act on.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum ArrowVal<V> {
    /// A payload leaf.
    Leaf(V),
    /// A product node — the pair the strength combinators operate on.
    Pair(Box<ArrowVal<V>>, Box<ArrowVal<V>>),
    /// A left injection — the sum node the choice combinators route on (`⊕`, the coproduct
    /// counterpart of `Pair`).
    InL(Box<ArrowVal<V>>),
    /// A right injection — the other summand of the sum node.
    InR(Box<ArrowVal<V>>),
}

impl<V> ArrowVal<V> {
    /// Builds a [`ArrowVal::Pair`] without writing the `Box`es.
    #[inline]
    pub fn pair(left: ArrowVal<V>, right: ArrowVal<V>) -> Self {
        ArrowVal::Pair(Box::new(left), Box::new(right))
    }

    /// Builds a [`ArrowVal::InL`] (left injection) without writing the `Box`.
    #[inline]
    pub fn inl(value: ArrowVal<V>) -> Self {
        ArrowVal::InL(Box::new(value))
    }

    /// Builds a [`ArrowVal::InR`] (right injection) without writing the `Box`.
    #[inline]
    pub fn inr(value: ArrowVal<V>) -> Self {
        ArrowVal::InR(Box::new(value))
    }
}

/// The **erased core**: the free arrow over a generator set `G`, stored as first-order data.
///
/// Every strong-category generator is a variant; recursion goes through `alloc::boxed::Box` (a
/// concrete type — no `dyn`). This is what a [`ArrowTerm`] lowers to, and what
/// [`interpret`](ArrowCore::interpret) folds. The object types are erased, so the tree is uniform
/// and storable; type-safe *construction* is recovered by the [`ArrowTerm`] façade.
#[derive(Clone, Debug, PartialEq, Eq)]
pub enum ArrowCore<G> {
    /// The identity arrow.
    Id,
    /// A generator drawn from the generating set `G`.
    Gen(G),
    /// `f >>> g` — run `f`, then `g`.
    Compose(Box<ArrowCore<G>>, Box<ArrowCore<G>>),
    /// `first f` — act on the left of a pair, pass the right through.
    First(Box<ArrowCore<G>>),
    /// `second g` — act on the right of a pair, pass the left through.
    Second(Box<ArrowCore<G>>),
    /// `f *** g` — act on both sides of a pair independently.
    Split(Box<ArrowCore<G>>, Box<ArrowCore<G>>),
    /// `f &&& g` — copy the input and feed it to both.
    Fanout(Box<ArrowCore<G>>, Box<ArrowCore<G>>),
    /// `left f` — act on the left summand of a sum, pass a right injection through (`⊕`).
    Left(Box<ArrowCore<G>>),
    /// `right g` — act on the right summand of a sum, pass a left injection through.
    Right(Box<ArrowCore<G>>),
    /// `f +++ g` — route each summand of a sum to its own arm.
    Choice(Box<ArrowCore<G>>, Box<ArrowCore<G>>),
    /// `f ||| g` — the coproduct elimination: route each summand to its arm and **unwrap** the
    /// injection (both arms converge on one output).
    Fanin(Box<ArrowCore<G>>, Box<ArrowCore<G>>),
}

impl<G> ArrowCore<G> {
    /// Interprets the term over [`ArrowVal`], extending an interpretation of the **generators**
    /// homomorphically over the whole strong category.
    ///
    /// `interp` maps a generator and a leaf payload to a new payload (a leaf endomorphism); the
    /// extension is forced by the combinator structure: `Compose` sequences, `Split`/`First`/
    /// `Second` act componentwise on a `Pair`, `Fanout` copies the input. This *is* the free
    /// arrow's universal property — the result depends only on `interp`'s action on the generators
    /// (`haft.arrow_term.free`), and it agrees with running the corresponding eager
    /// [`Arrow`](crate::Arrow) combinators (`haft.arrow_term.interpret_sound`).
    ///
    /// A combinator applied to a value of the wrong shape (e.g. `First` on a `Leaf`) passes the
    /// value through unchanged; the [`ArrowTerm`] façade makes such a mismatch unreachable for
    /// terms fed their declared input shape.
    pub fn interpret<V, I>(&self, interp: &I, input: ArrowVal<V>) -> ArrowVal<V>
    where
        I: Fn(&G, V) -> V,
        V: Clone,
    {
        match self {
            ArrowCore::Id => input,
            ArrowCore::Gen(g) => match input {
                ArrowVal::Leaf(v) => ArrowVal::Leaf(interp(g, v)),
                other @ (ArrowVal::Pair(..) | ArrowVal::InL(_) | ArrowVal::InR(_)) => other,
            },
            ArrowCore::Compose(f, g) => g.interpret(interp, f.interpret(interp, input)),
            ArrowCore::First(f) => match input {
                ArrowVal::Pair(a, b) => ArrowVal::Pair(Box::new(f.interpret(interp, *a)), b),
                other @ (ArrowVal::Leaf(_) | ArrowVal::InL(_) | ArrowVal::InR(_)) => other,
            },
            ArrowCore::Second(g) => match input {
                ArrowVal::Pair(a, b) => ArrowVal::Pair(a, Box::new(g.interpret(interp, *b))),
                other @ (ArrowVal::Leaf(_) | ArrowVal::InL(_) | ArrowVal::InR(_)) => other,
            },
            ArrowCore::Split(f, g) => match input {
                ArrowVal::Pair(a, b) => ArrowVal::Pair(
                    Box::new(f.interpret(interp, *a)),
                    Box::new(g.interpret(interp, *b)),
                ),
                other @ (ArrowVal::Leaf(_) | ArrowVal::InL(_) | ArrowVal::InR(_)) => other,
            },
            ArrowCore::Fanout(f, g) => ArrowVal::Pair(
                Box::new(f.interpret(interp, input.clone())),
                Box::new(g.interpret(interp, input)),
            ),
            // The choice fragment (⊕): route on the sum node. `Left`/`Right` act on their summand
            // and pass the other injection through; `Choice` routes both; `Fanin` routes and
            // UNWRAPS the injection (the coproduct elimination — both arms converge).
            ArrowCore::Left(f) => match input {
                ArrowVal::InL(a) => ArrowVal::InL(Box::new(f.interpret(interp, *a))),
                other @ (ArrowVal::Leaf(_) | ArrowVal::Pair(..) | ArrowVal::InR(_)) => other,
            },
            ArrowCore::Right(g) => match input {
                ArrowVal::InR(b) => ArrowVal::InR(Box::new(g.interpret(interp, *b))),
                other @ (ArrowVal::Leaf(_) | ArrowVal::Pair(..) | ArrowVal::InL(_)) => other,
            },
            ArrowCore::Choice(f, g) => match input {
                ArrowVal::InL(a) => ArrowVal::InL(Box::new(f.interpret(interp, *a))),
                ArrowVal::InR(b) => ArrowVal::InR(Box::new(g.interpret(interp, *b))),
                other @ (ArrowVal::Leaf(_) | ArrowVal::Pair(..)) => other,
            },
            ArrowCore::Fanin(f, g) => match input {
                ArrowVal::InL(a) => f.interpret(interp, *a),
                ArrowVal::InR(b) => g.interpret(interp, *b),
                other @ (ArrowVal::Leaf(_) | ArrowVal::Pair(..)) => other,
            },
        }
    }
}

/// The typed façade over [`ArrowCore`]: a free-arrow term whose `In`/`Out` objects are tracked in
/// the type so that only sound wiring composes.
///
/// The objects are phantom (via `fn(In) -> Out`, keeping the term invariant and requiring no
/// ownership of `In`/`Out`); the runtime payload is entirely the erased [`ArrowCore`]. Build with
/// [`id`](ArrowTerm::id) / [`generator`](ArrowTerm::generator) and grow with
/// [`compose`](ArrowTerm::compose), [`first`](ArrowTerm::first), [`second`](ArrowTerm::second),
/// [`split`](ArrowTerm::split), [`fanout`](ArrowTerm::fanout); reach the core with
/// [`core`](ArrowTerm::core) / [`into_core`](ArrowTerm::into_core).
pub struct ArrowTerm<In, Out, G> {
    core: ArrowCore<G>,
    _wiring: PhantomData<fn(In) -> Out>,
}

impl<In, Out, G> ArrowTerm<In, Out, G> {
    #[inline]
    const fn wrap(core: ArrowCore<G>) -> Self {
        ArrowTerm {
            core,
            _wiring: PhantomData,
        }
    }

    /// Lifts a single generator into a term `In → Out`. The caller fixes the objects; the erased
    /// core stores only the generator.
    #[inline]
    pub const fn generator(g: G) -> Self {
        ArrowTerm::wrap(ArrowCore::Gen(g))
    }

    /// Borrows the erased core for inspection or interpretation.
    #[inline]
    pub const fn core(&self) -> &ArrowCore<G> {
        &self.core
    }

    /// Consumes the term, yielding the erased core for storage or rewriting.
    #[inline]
    pub fn into_core(self) -> ArrowCore<G> {
        self.core
    }
}

impl<A, G> ArrowTerm<A, A, G> {
    /// The identity term `A → A`.
    #[inline]
    pub const fn id() -> Self {
        ArrowTerm::wrap(ArrowCore::Id)
    }
}

impl<In, Out, G> ArrowTerm<In, Out, G> {
    /// Sequential composition `self >>> next`. The middle object `Out` must match `next`'s input,
    /// so a mismatched pipeline does not compile.
    #[inline]
    pub fn compose<Next>(self, next: ArrowTerm<Out, Next, G>) -> ArrowTerm<In, Next, G> {
        ArrowTerm::wrap(ArrowCore::Compose(Box::new(self.core), Box::new(next.core)))
    }

    /// `first`: lift `In → Out` to `(In, C) → (Out, C)`, passing the right component through.
    #[inline]
    pub fn first<C>(self) -> ArrowTerm<(In, C), (Out, C), G> {
        ArrowTerm::wrap(ArrowCore::First(Box::new(self.core)))
    }

    /// `second`: lift `In → Out` to `(C, In) → (C, Out)`, passing the left component through.
    #[inline]
    pub fn second<C>(self) -> ArrowTerm<(C, In), (C, Out), G> {
        ArrowTerm::wrap(ArrowCore::Second(Box::new(self.core)))
    }

    /// The monoidal product `self *** g`: `(In, I2) → (Out, O2)`.
    #[inline]
    pub fn split<I2, O2>(self, g: ArrowTerm<I2, O2, G>) -> ArrowTerm<(In, I2), (Out, O2), G> {
        ArrowTerm::wrap(ArrowCore::Split(Box::new(self.core), Box::new(g.core)))
    }

    /// Fanout `self &&& g`: feed one input to both — `In → (Out, O2)`.
    #[inline]
    pub fn fanout<O2>(self, g: ArrowTerm<In, O2, G>) -> ArrowTerm<In, (Out, O2), G> {
        ArrowTerm::wrap(ArrowCore::Fanout(Box::new(self.core), Box::new(g.core)))
    }

    /// `left`: lift `In → Out` to `Either<In, C> → Either<Out, C>`, passing a right injection
    /// through (the choice fragment `⊕`; Hughes 2000 §5).
    #[inline]
    pub fn left<C>(self) -> ArrowTerm<crate::Either<In, C>, crate::Either<Out, C>, G> {
        ArrowTerm::wrap(ArrowCore::Left(Box::new(self.core)))
    }

    /// `right`: lift `In → Out` to `Either<C, In> → Either<C, Out>`, passing a left injection
    /// through.
    #[inline]
    pub fn right<C>(self) -> ArrowTerm<crate::Either<C, In>, crate::Either<C, Out>, G> {
        ArrowTerm::wrap(ArrowCore::Right(Box::new(self.core)))
    }

    /// The coproduct sum `self +++ g`: `Either<In, I2> → Either<Out, O2>`.
    #[inline]
    pub fn choice<I2, O2>(
        self,
        g: ArrowTerm<I2, O2, G>,
    ) -> ArrowTerm<crate::Either<In, I2>, crate::Either<Out, O2>, G> {
        ArrowTerm::wrap(ArrowCore::Choice(Box::new(self.core), Box::new(g.core)))
    }

    /// Fanin `self ||| g`: the coproduct elimination — both branches converge on `Out`, so the
    /// branch outputs must agree: `Either<In, I2> → Out`. Mistyped branch wiring fails to compile:
    ///
    /// ```compile_fail
    /// use deep_causality_haft::ArrowTerm;
    /// #[derive(Clone)]
    /// struct Op;
    /// let int_branch = ArrowTerm::<i64, i64, Op>::generator(Op);   // Out = i64
    /// let pair_branch = ArrowTerm::<u8, u8, Op>::generator(Op)
    ///     .first::<u8>();                                          // Out = (u8, u8)
    /// // i64 ≠ (u8, u8) — the branch outputs do not converge.
    /// let _bad = int_branch.fanin(pair_branch);
    /// ```
    #[inline]
    pub fn fanin<I2>(self, g: ArrowTerm<I2, Out, G>) -> ArrowTerm<crate::Either<In, I2>, Out, G> {
        ArrowTerm::wrap(ArrowCore::Fanin(Box::new(self.core), Box::new(g.core)))
    }
}