233: Curry-Howard Correspondence

/// Curry-Howard correspondence: propositions are types, proofs are programs.
///
/// - A -> B         corresponds to a function `fn(A) -> B`
/// - A /\ B (And)   corresponds to a pair `(A, B)`
/// - A \/ B (Or)    corresponds to `Result<A, B>` or an enum
/// - True           corresponds to `()` (unit — trivially inhabited)
/// - False          corresponds to `!` (never — uninhabited)
/// - Not A          corresponds to `fn(A) -> !` (a function to Never)
///
/// A "proof" of a proposition is a value of the corresponding type.
/// If a type is inhabited (has a value), the proposition is provable.

// ── Conjunction (A ∧ B) ──────────────────────────────────────────────────────

/// Proof of "A and B": we must provide both A and B.
struct And<A, B>(A, B);

fn and_intro<A, B>(a: A, b: B) -> And<A, B> {
    And(a, b)
}

fn and_elim_left<A: Clone, B>(proof: &And<A, B>) -> A {
    proof.0.clone()
}

fn and_elim_right<A, B: Clone>(proof: &And<A, B>) -> B {
    proof.1.clone()
}

// ── Disjunction (A ∨ B) ──────────────────────────────────────────────────────

/// Proof of "A or B": we provide either A or B (but not necessarily both).
/// In Rust, `Result<A, B>` (or any enum) serves this role.
/// We use our own type for clarity.
enum Or<A, B> {
    Left(A),
    Right(B),
}

fn or_intro_left<A, B>(a: A) -> Or<A, B> {
    Or::Left(a)
}

fn or_intro_right<A, B>(b: B) -> Or<A, B> {
    Or::Right(b)
}

fn or_elim<A, B, C>(or: Or<A, B>, f: impl Fn(A) -> C, g: impl Fn(B) -> C) -> C {
    match or {
        Or::Left(a) => f(a),
        Or::Right(b) => g(b),
    }
}

// ── Implication (A → B) ──────────────────────────────────────────────────────

/// Modus ponens: given a proof of A->B and a proof of A, produce proof of B.
fn modus_ponens<A, B>(f: impl Fn(A) -> B, a: A) -> B {
    f(a)
}

// ── Negation (¬A = A → ⊥) ────────────────────────────────────────────────────

/// Negation as a function to the never type.
/// In stable Rust, `!` (Never) cannot be used in all positions yet,
/// so we use a phantom approach. In nightly `!` is fully usable.
///
/// We model ¬A as: a proof that A leads to contradiction.
/// Since we can't easily use `!` as a return type in stable Rust for trait objects,
/// we demonstrate the concept with a marker.
struct Not<A>(std::marker::PhantomData<fn(A) -> std::convert::Infallible>);

/// Double negation introduction: A ⊢ ¬¬A
/// Given a proof of A, we can always produce a proof of ¬¬A.
/// (The converse — double-negation elimination — requires classical logic.)
fn double_neg_intro<A>(_proof_of_a: &A) -> Box<dyn Fn(&dyn Fn(&A)) -> ()> {
    // ¬¬A = (A -> False) -> False
    // We return a function that takes (¬A) and applies it to our A.
    // In constructive logic, this is valid: given A, give me ¬A and I'll derive ⊥.
    Box::new(|_neg_a: &dyn Fn(&A)| {
        // neg_a(_proof_of_a) would be ⊥, but we can't fully express this without !
        // The type-level encoding shows the structure is correct.
    })
}

// ── Some actual proofs ────────────────────────────────────────────────────────

/// Proof: A ∧ B → B ∧ A  (conjunction is commutative)
fn and_comm<A: Clone, B: Clone>(proof: And<A, B>) -> And<B, A> {
    And(proof.1, proof.0)
}

/// Proof: A → A  (identity / reflexivity)
fn identity_proof<A>(a: A) -> A {
    a
}

/// Proof: A ∧ (A → B) → B  (modus ponens as a conjunction)
fn and_modus_ponens<A: Clone, B>(proof: And<A, impl Fn(A) -> B>) -> B {
    (proof.1)(proof.0)
}

/// Proof: (A ∨ B) ∧ ¬A → B
/// If we have "A or B" and "not A", then we must have B.
fn disjunctive_syllogism<A, B>(
    or_proof: Or<A, B>,
    _refutation: impl Fn(A) -> B,  // ¬A = A -> contradiction-ish
) -> B {
    match or_proof {
        Or::Left(a) => _refutation(a),
        Or::Right(b) => b,
    }
}

fn main() {
    println!("=== Curry-Howard Correspondence ===\n");
    println!("Propositions are types. Proofs are programs.\n");

    // Proof of "Int AND String"
    let conj = and_intro(42_i32, "hello");
    let left = and_elim_left(&conj);
    let right = and_elim_right(&conj);
    println!("And(42, \"hello\"): left={}, right={}", left, right);

    // Commutativity of And
    let swapped = and_comm(and_intro(1_i32, "world"));
    println!("and_comm: ({}, {})", swapped.0, swapped.1);

    // Proof of "Int OR String" via left injection
    let disj: Or<i32, &str> = or_intro_left(42);
    let result = or_elim(disj, |n| format!("number: {}", n), |s| format!("string: {}", s));
    println!("Or::Left(42): {}", result);

    // Modus ponens: we have proof of A and proof of A->B, so B
    let mp_result = modus_ponens(|n: i32| n * 2, 21);
    println!("Modus ponens (21 * 2 = {})", mp_result);

    // Identity: proof that A -> A always holds
    let id_result = identity_proof(99_i32);
    println!("Identity proof: {}", id_result);

    println!();
    println!("Key insight: if a function type is inhabited (has an implementation),");
    println!("the corresponding logical implication is provable.");
    println!("fn(A) -> B  ≡  A implies B");
    println!("fn(A) -> !  ≡  A is false (A implies absurdity)");
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_and_intro_elim() {
        let proof = and_intro(10_i32, "ten");
        assert_eq!(and_elim_left(&proof), 10);
        assert_eq!(and_elim_right(&proof), "ten");
    }

    #[test]
    fn test_and_comm() {
        let proof = and_intro(1_i32, 2_i32);
        let swapped = and_comm(proof);
        assert_eq!(swapped.0, 2);
        assert_eq!(swapped.1, 1);
    }

    #[test]
    fn test_or_elim() {
        let left: Or<i32, &str> = or_intro_left(42);
        let r = or_elim(left, |n| n * 2, |_| 0);
        assert_eq!(r, 84);

        let right: Or<i32, i32> = or_intro_right(7);
        let r2 = or_elim(right, |n| n + 100, |n| n + 1);
        assert_eq!(r2, 8);
    }

    #[test]
    fn test_modus_ponens() {
        let result = modus_ponens(|s: &str| s.len(), "hello");
        assert_eq!(result, 5);
    }

    #[test]
    fn test_identity() {
        assert_eq!(identity_proof(42_i32), 42);
        assert_eq!(identity_proof("hello"), "hello");
    }
}