csw-core 0.1.0

Core categorical structures for the Categorical Semantics Workbench - define categories and derive type systems
Documentation

csw-core

Core categorical structures for the Categorical Semantics Workbench.

This crate provides the foundational types for specifying categorical structures (products, coproducts, exponentials, tensor products, etc.) and their properties. From these specifications, type systems can be automatically derived using the Curry-Howard-Lambek correspondence.

Overview

The Categorical Semantics Workbench operationalizes the fundamental insight:

Category Theory Logic Type Theory
Objects Propositions Types
Morphisms Proofs Terms/Programs
Products A × B Conjunction A ∧ B Pair types (A, B)
Coproducts A + B Disjunction A ∨ B Sum types Either<A, B>
Exponentials B^A Implication A → B Function types A → B
Tensor A ⊗ B Linear conjunction Linear pairs
Linear hom A ⊸ B Linear implication Linear functions

Usage

use csw_core::CategoryBuilder;

// Define a Cartesian Closed Category (CCC)
// This derives the Simply-Typed Lambda Calculus
let ccc = CategoryBuilder::new("STLC")
    .with_base("Int")
    .with_base("Bool")
    .with_terminal()
    .with_products()
    .with_exponentials()
    .cartesian()
    .build()
    .expect("valid CCC specification");

// Define a Symmetric Monoidal Closed Category (SMCC)
// This derives the Linear Lambda Calculus
let smcc = CategoryBuilder::new("Linear")
    .with_base("Int")
    .with_tensor()
    .with_linear_hom()
    .with_symmetry()
    .linear()
    .build()
    .expect("valid SMCC specification");

// Define an Affine Category (Rust-like ownership)
let affine = CategoryBuilder::new("Affine")
    .with_tensor()
    .with_linear_hom()
    .affine()  // can drop, cannot clone
    .build()
    .expect("valid affine specification");

Structural Rules

The presence or absence of certain categorical structures determines which structural rules are available:

Structure Structural Rule Effect
Diagonal Δ: A → A × A Contraction Variables can be used multiple times
Terminal !: A → 1 Weakening Variables can be ignored
Symmetry σ: A × B → B × A Exchange Variable order doesn't matter
  • Cartesian: Full structural rules (copy + drop + reorder)
  • Linear: No copying, no dropping (use exactly once)
  • Affine: Can drop but not copy (use at most once) — like Rust
  • Relevant: Can copy but not drop (use at least once)

License

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