Struct FreeTheoremDeriver 

pub struct FreeTheoremDeriver {
    pub type_sig: String,
    pub theorem: String,
}

Derives (schematic) free theorems for polymorphic functions on lists.

Given the type ∀ α. List α → List α, the free theorem states that for any function h : A → B and parametric f: map h (f xs) = f (map h xs)

Fields

type_sig: String

The polymorphic type signature (as a string description)

theorem: String

The derived free theorem (as a string description)

Implementations

impl FreeTheoremDeriver

pub fn list_endomorphism() -> Self

Derive the free theorem for ∀ α. List α → List α.

pub fn poly_identity() -> Self

Derive the free theorem for ∀ α. α → α (parametric identity).

pub fn poly_map() -> Self

Derive the free theorem for ∀ α β. (α → β) → List α → List β (parametric map).

pub fn verify_identity_theorem(xs: Vec<i32>) -> bool

Verify the stated free theorem holds for a concrete list operation.

Uses a simplified test: map id xs = xs for the identity theorem.

pub fn verify_reverse_naturality<A: Clone, B: Clone>( f: impl Fn(A) -> B, xs: Vec<A>, ) -> bool

Verify the naturality of reverse: reverse (map f xs) = map f (reverse xs).