deep_causality_haft 0.4.3

HKT traits for for the deep_causality crate.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78

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

use crate::{HKT2Unbound, Satisfies};

/// The `Profunctor` trait represents a type constructor that is contravariant in its first argument
/// and covariant in its second argument.
///
/// # Category Theory
/// A **Profunctor** is a functor $P: \mathcal{C}^{op} \times \mathcal{D} \to \text{Set}$.
/// It can be thought of as a generalized function $A \to B$, where you can pre-process the input $A$
/// and post-process the output $B$.
///
/// *   **Dimap**: $(C \to A) \to (B \to D) \to P(A, B) \to P(C, D)$
///
/// # Mathematical Definition
/// Let $P$ be a profunctor. For morphisms $f: C \to A$ (pre-composition) and $g: B \to D$ (post-composition),
/// `dimap` yields a morphism $P(A, B) \to P(C, D)$.
///
/// # Laws (Informal)
///
/// The functor laws of $P: \mathcal{C}^{op} \times \mathcal{D} \to \text{Set}$:
///
/// 1.  **Identity**: `dimap(p, id, id) == p`
/// 2.  **Composition** (note the contravariant twist on the first argument):
///     `dimap(dimap(p, pre, post), pre2, post2) == dimap(p, |a| pre(pre2(a)), |b| post2(post(b)))`
///     — pre-processors compose in reversed order, post-processors compose forward.
///
/// Laws are stated for pure functions; a stateful `FnMut` closure voids them.
/// Machine-checked in `lean/DeepCausalityFormal/Haft/Profunctor.lean`.
///
/// # Use Cases
/// *   **Adapters**: Wrapping a core logic kernel with input decoders and output encoders.
/// *   **Optics**: Used heavily in Lens libraries to access and modify nested data structures.
/// *   **State Machines**: Transforming the input alphabet and output alphabet of a transducer.
pub trait Profunctor<P: HKT2Unbound> {
    /// Contravariant map on A (Input), Covariant map on B (Output).
    /// "Pre-process the input, Post-process the output."
    ///
    /// # Arguments
    /// * `pab`: The profunctor instance `P<A, B>`.
    /// * `f_pre`: The pre-processing function `C -> A`.
    /// * `f_post`: The post-processing function `B -> D`.
    fn dimap<A, B, C, D, F1, F2>(pab: P::Type<A, B>, f_pre: F1, f_post: F2) -> P::Type<C, D>
    where
        A: 'static + Satisfies<P::Constraint>,
        B: 'static + Satisfies<P::Constraint>,
        C: 'static + Satisfies<P::Constraint>,
        D: 'static + Satisfies<P::Constraint>,
        F1: FnMut(C) -> A + 'static,
        F2: FnMut(B) -> D + 'static;

    /// Map only the input (Contravariant).
    /// Equivalent to `dimap(f, id)`.
    fn lmap<A, B, C, F1>(pab: P::Type<A, B>, f_pre: F1) -> P::Type<C, B>
    where
        A: 'static + Satisfies<P::Constraint>,
        B: 'static + Satisfies<P::Constraint> + Clone,
        C: 'static + Satisfies<P::Constraint>,
        F1: FnMut(C) -> A + 'static,
    {
        Self::dimap(pab, f_pre, |b| b)
    }

    /// Map only the output (Covariant).
    /// Equivalent to `dimap(id, g)`.
    fn rmap<A, B, D, F2>(pab: P::Type<A, B>, f_post: F2) -> P::Type<A, D>
    where
        A: 'static + Satisfies<P::Constraint> + Clone,
        B: 'static + Satisfies<P::Constraint>,
        D: 'static + Satisfies<P::Constraint>,
        F2: FnMut(B) -> D + 'static,
    {
        Self::dimap(pab, |a| a, f_post)
    }
}