csw-derive

Type system derivation engine for the Categorical Semantics Workbench.

This crate implements the Curry-Howard-Lambek correspondence as an automated construction: given a categorical structure specification, it derives the corresponding type system with 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

Usage

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

// Define a Cartesian Closed Category
let ccc = CategoryBuilder::new("STLC")
    .with_base("Int")
    .with_base("Bool")
    .with_terminal()
    .with_products()
    .with_exponentials()
    .cartesian()
    .build()
    .unwrap();

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

// Print the derived type system
println!("{}", type_system);

Derived Outputs

A TypeSystem contains:

Type constructors: How to form types (Unit, Product, Arrow, etc.)
Term constructors: How to form terms (variables, pairs, lambdas, etc.)
Typing rules: Inference rules for type checking
Reduction rules: β-reduction rules for evaluation
Equivalence rules: η-expansion rules
Structural rules: Weakening, contraction, exchange

Example Output

For a CCC specification, the derivation produces:

Types:
  τ ::= Int | Bool | 1 | τ × τ | τ → τ

Terms:
  e ::= x | () | (e, e) | fst e | snd e | λx.e | e e

Typing Rules:
  Γ ⊢ () : 1                              (unit-intro)
  Γ ⊢ a : A    Γ ⊢ b : B
  ────────────────────────                (pair-intro)
  Γ ⊢ (a, b) : A × B
  ...

Structural Rules:
  Weakening:   ✓
  Contraction: ✓
  Exchange:    ✓

License