Crate csw_derive 

csw-derive

Type system derivation engine for the Categorical Semantics Workbench.

This crate implements the Curry-Howard-Lambek correspondence as a construction: given a categorical structure specification, it automatically derives the corresponding type system with its typing rules, reduction rules, and structural properties.

Overview

The derivation process transforms categorical structures into type systems:

Categorical Structure	Derived Type System
Terminal object	Unit type (1)
Products (A × B)	Pair types with fst/snd
Coproducts (A + B)	Sum types with case
Exponentials (B^A)	Function types (A → B)
Tensor (A ⊗ B)	Linear pairs
Linear hom (A ⊸ B)	Linear functions

Example

use csw_core::CategoryBuilder;
use csw_derive::Deriver;

// Define a CCC
let ccc = CategoryBuilder::new("STLC")
    .with_terminal()
    .with_products()
    .with_exponentials()
    .cartesian()
    .build()
    .unwrap();

// Derive the type system
let type_system = Deriver::derive(&ccc);

// The result contains:
// - Type constructors: 1, ×, →
// - Term constructors: (), (,), fst, snd, λ, application
// - Typing rules for each constructor
// - β-reduction rules
// - η-expansion rules

Structs

Deriver

The main derivation engine.

EquivalenceRule

An equivalence rule (η-expansion).

ReductionRule

A reduction rule (β-reduction).

StructuralRules

Structural rules available in the type system.

TermConstructor

A term constructor in the derived type system.

TypeConstructor

A type constructor in the derived type system.

TypeSystem

A complete derived type system.

TypingRule

A typing rule in the type system.

Enums

TermConstructorKind

The kind of a term constructor.

TypeConstructorKind

The kind of a type constructor.