csw_derive/lib.rs
1//! # csw-derive
2//!
3//! Type system derivation engine for the Categorical Semantics Workbench.
4//!
5//! This crate implements the Curry-Howard-Lambek correspondence as a construction:
6//! given a categorical structure specification, it automatically derives the
7//! corresponding type system with its typing rules, reduction rules, and structural properties.
8//!
9//! ## Overview
10//!
11//! The derivation process transforms categorical structures into type systems:
12//!
13//! | Categorical Structure | Derived Type System |
14//! |-----------------------|---------------------|
15//! | Terminal object | Unit type (1) |
16//! | Products (A × B) | Pair types with fst/snd |
17//! | Coproducts (A + B) | Sum types with case |
18//! | Exponentials (B^A) | Function types (A → B) |
19//! | Tensor (A ⊗ B) | Linear pairs |
20//! | Linear hom (A ⊸ B) | Linear functions |
21//!
22//! ## Example
23//!
24//! ```rust
25//! use csw_core::CategoryBuilder;
26//! use csw_derive::Deriver;
27//!
28//! // Define a CCC
29//! let ccc = CategoryBuilder::new("STLC")
30//! .with_terminal()
31//! .with_products()
32//! .with_exponentials()
33//! .cartesian()
34//! .build()
35//! .unwrap();
36//!
37//! // Derive the type system
38//! let type_system = Deriver::derive(&ccc);
39//!
40//! // The result contains:
41//! // - Type constructors: 1, ×, →
42//! // - Term constructors: (), (,), fst, snd, λ, application
43//! // - Typing rules for each constructor
44//! // - β-reduction rules
45//! // - η-expansion rules
46//! ```
47
48#![warn(missing_docs)]
49#![warn(rustdoc::missing_crate_level_docs)]
50
51mod type_system;
52mod derivation;
53
54pub use type_system::*;
55pub use derivation::*;