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:

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

Licensed under either of Apache License, Version 2.0 or MIT license at your option.