142: Type Equality Witnesses

// Type equality witnesses: a value of type TypeEq<A, B> proves A = B.
//
// In OCaml/Haskell this is used with GADTs to unify type variables.
// Rust doesn't have GADTs, but we can:
//   1. Define TypeEq<A, B> that can only be constructed for TypeEq<T, T>
//   2. Use it as a proof to safely coerce values
//   3. Show symmetry and transitivity
//
// The key insight: TypeEq::refl() is only callable when A = B (same type),
// so any function accepting a TypeEq<A, B> has a compile-time proof A = B.

use std::marker::PhantomData;

// ── Core TypeEq type ─────────────────────────────────────────────────────────

/// A witness that types `A` and `B` are equal.
/// Can only be constructed (via `refl`) when `A = B`.
pub struct TypeEq<A, B>(PhantomData<(A, B)>);

impl<T> TypeEq<T, T> {
    /// Construct a proof of `T = T` (reflexivity).
    pub fn refl() -> TypeEq<T, T> {
        TypeEq(PhantomData)
    }
}

impl<A, B> TypeEq<A, B> {
    /// Symmetry: if A = B then B = A.
    pub fn sym(self) -> TypeEq<B, A> {
        TypeEq(PhantomData)
    }

    /// Transitivity: if A = B and B = C then A = C.
    pub fn trans<C>(self, _other: TypeEq<B, C>) -> TypeEq<A, C> {
        TypeEq(PhantomData)
    }

    /// Lift the equality through a container: if A = B then Vec<A> = Vec<B>.
    /// (We can't fully express this in Rust without HKT, but see coerce below.)
    pub fn coerce(self, a: A) -> B
    where
        A: Into<B>,
    {
        a.into()
    }
}

impl<T: Clone> TypeEq<T, T> {
    /// Use the proof to safely "cast" (here: copy) a value.
    pub fn cast(&self, a: T) -> T {
        a
    }
}

// ── Leibniz-style equality ───────────────────────────────────────────────────
// Leibniz: A = B iff for all P, P(A) → P(B).
// In Rust we approximate this with a concrete container.

pub struct Leibniz<A, B> {
    /// The coercion function: given any P<A>, produce P<B>.
    /// We use Box<A> -> Box<B> as a concrete instantiation.
    coerce: Box<dyn Fn(Box<A>) -> Box<B>>,
}

impl<T: 'static> Leibniz<T, T> {
    pub fn refl() -> Self {
        Leibniz { coerce: Box::new(|x| x) }
    }
}

impl<A: 'static, B: 'static> Leibniz<A, B> {
    pub fn apply(&self, a: A) -> B {
        *((self.coerce)(Box::new(a)))
    }
}

// ── Type-tagged value (shows coercion in action) ─────────────────────────────

/// A value tagged with a phantom type.
#[derive(Debug, PartialEq)]
pub struct Tagged<Tag, Val> {
    pub value: Val,
    _tag: PhantomData<Tag>,
}

impl<Tag, Val> Tagged<Tag, Val> {
    pub fn new(value: Val) -> Self {
        Tagged { value, _tag: PhantomData }
    }
}

/// Given TypeEq<A, A>, coerce Tagged<A, V> (trivially).
pub fn coerce_tag<A, V>(
    _eq: TypeEq<A, A>,
    t: Tagged<A, V>,
) -> Tagged<A, V> {
    t // the proof tells us the tags are the same type
}

// ── Demonstration: use TypeEq in generic code ────────────────────────────────

/// A function that, given proof that S = String, turns any S into its length.
fn length_if_string<S>(value: S, _proof: TypeEq<S, String>) -> usize
where
    S: Into<String>,
{
    Into::<String>::into(value).len()
}

fn main() {
    // Reflexivity
    let eq: TypeEq<i32, i32> = TypeEq::refl();
    let n: i32 = 42;
    let m = eq.cast(n);
    assert_eq!(n, m);
    println!("cast_with Refl: {}", m);

    // Symmetry
    let eq2: TypeEq<i32, i32> = TypeEq::refl();
    let _sym: TypeEq<i32, i32> = eq2.sym();
    println!("symmetry holds (TypeEq<i32,i32>.sym() = TypeEq<i32,i32>)");

    // Transitivity
    let eq_ab: TypeEq<i32, i32> = TypeEq::refl();
    let eq_bc: TypeEq<i32, i32> = TypeEq::refl();
    let _eq_ac: TypeEq<i32, i32> = eq_ab.trans(eq_bc);
    println!("transitivity holds");

    // Use proof to coerce String -> String
    let proof: TypeEq<String, String> = TypeEq::refl();
    let len = length_if_string("hello".to_string(), proof);
    println!("length_if_string: {}", len);

    // Tagged coercion
    let tagged = Tagged::<i32, &str>::new("world");
    let eq3: TypeEq<i32, i32> = TypeEq::refl();
    let tagged2 = coerce_tag(eq3, tagged);
    println!("Tagged value: {}", tagged2.value);

    // Leibniz equality
    let leib: Leibniz<String, String> = Leibniz::refl();
    let result = leib.apply("hello".to_string());
    println!("Leibniz coerce: {}", result);

    println!("Type equality proofs work");
}

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

    #[test]
    fn test_refl_cast() {
        let eq: TypeEq<String, String> = TypeEq::refl();
        let s = "hello".to_string();
        assert_eq!(eq.cast(s.clone()), s);
    }

    #[test]
    fn test_sym() {
        let eq: TypeEq<i32, i32> = TypeEq::refl();
        let _sym: TypeEq<i32, i32> = eq.sym();
        // compiles and runs ⟹ symmetry works
    }

    #[test]
    fn test_trans() {
        let ab: TypeEq<u8, u8> = TypeEq::refl();
        let bc: TypeEq<u8, u8> = TypeEq::refl();
        let _ac: TypeEq<u8, u8> = ab.trans(bc);
    }

    #[test]
    fn test_length_if_string() {
        let proof: TypeEq<String, String> = TypeEq::refl();
        assert_eq!(length_if_string("rust".to_string(), proof), 4);
    }

    #[test]
    fn test_leibniz() {
        let leib: Leibniz<i32, i32> = Leibniz::refl();
        assert_eq!(leib.apply(42_i32), 42_i32);
    }
}