1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
//! # 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
//!
//! ```rust
//! 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
//! ```
pub use *;
pub use *;