csw_core/
category.rs

1//! Core categorical specification types.
2
3#[cfg(feature = "serde")]
4use serde::{Deserialize, Serialize};
5
6/// A specification of categorical structure.
7///
8/// This is the main type representing a category with its structural features.
9/// From this specification, a type system can be derived.
10#[derive(Clone, Debug, PartialEq, Eq)]
11#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
12pub struct CategorySpec {
13    /// Name of the category/type system
14    pub name: String,
15
16    /// Base objects (primitive types)
17    pub base_objects: Vec<BaseObject>,
18
19    /// Structural features present in the category
20    pub structure: StructuralFeatures,
21}
22
23/// A base/primitive object in the category.
24///
25/// These become the ground types in the derived type system.
26#[derive(Clone, Debug, PartialEq, Eq)]
27#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
28pub struct BaseObject {
29    /// Name of the base type
30    pub name: String,
31
32    /// Optional description
33    pub description: Option<String>,
34}
35
36/// Structural features present in a category.
37///
38/// These determine what type constructors and structural rules
39/// will be present in the derived type system.
40#[derive(Clone, Debug, Default, PartialEq, Eq)]
41#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
42pub struct StructuralFeatures {
43    // === Limits ===
44    /// Terminal object (unit type, 1)
45    pub terminal: bool,
46
47    /// Binary products (pair types, A × B)
48    pub products: bool,
49
50    /// Initial object (empty type, 0)
51    pub initial: bool,
52
53    /// Binary coproducts (sum types, A + B)
54    pub coproducts: bool,
55
56    // === Closed Structure ===
57    /// Exponentials (function types, A → B) - cartesian
58    pub exponentials: bool,
59
60    // === Monoidal Structure ===
61    /// Tensor product specification (A ⊗ B)
62    pub tensor: Option<TensorSpec>,
63
64    /// Linear hom / internal hom (A ⊸ B)
65    pub linear_hom: bool,
66
67    // === Structural Morphisms ===
68    /// Diagonal morphism availability (contraction)
69    pub diagonal: DiagonalSpec,
70
71    /// Terminal morphism availability (weakening)
72    pub terminal_morphism: TerminalSpec,
73
74    /// Symmetry/braiding (exchange rule)
75    pub symmetry: bool,
76}
77
78/// Specification for monoidal tensor product.
79#[derive(Clone, Debug, PartialEq, Eq)]
80#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
81pub struct TensorSpec {
82    /// Symbol for tensor (default: "⊗")
83    pub symbol: String,
84
85    /// Symbol for unit (default: "I")
86    pub unit_symbol: String,
87
88    /// Whether associativity is strict or weak
89    pub associativity: Associativity,
90}
91
92impl Default for TensorSpec {
93    fn default() -> Self {
94        Self {
95            symbol: "⊗".to_string(),
96            unit_symbol: "I".to_string(),
97            associativity: Associativity::Weak,
98        }
99    }
100}
101
102/// Associativity type for monoidal structure.
103#[derive(Clone, Debug, Default, PartialEq, Eq)]
104#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
105pub enum Associativity {
106    /// Strict associativity: (A ⊗ B) ⊗ C = A ⊗ (B ⊗ C)
107    Strict,
108    /// Weak associativity: (A ⊗ B) ⊗ C ≅ A ⊗ (B ⊗ C)
109    #[default]
110    Weak,
111}
112
113/// Specification for diagonal morphism (contraction/copying).
114#[derive(Clone, Debug, Default, PartialEq, Eq)]
115#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
116pub enum DiagonalSpec {
117    /// No diagonal (linear: cannot copy)
118    #[default]
119    None,
120    /// Diagonal for all objects (cartesian: can always copy)
121    Universal,
122    /// Diagonal only for specified objects
123    Restricted(Vec<String>),
124}
125
126/// Specification for terminal morphism (weakening/discarding).
127#[derive(Clone, Debug, Default, PartialEq, Eq)]
128#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
129pub enum TerminalSpec {
130    /// No terminal morphisms (relevant: cannot discard)
131    #[default]
132    None,
133    /// Terminal morphism for all objects (affine/cartesian: can always discard)
134    Universal,
135    /// Only for specified objects
136    Restricted(Vec<String>),
137}
138
139impl CategorySpec {
140    /// Returns true if this category has full structural rules (weakening + contraction + exchange).
141    pub fn is_cartesian(&self) -> bool {
142        matches!(self.structure.diagonal, DiagonalSpec::Universal)
143            && matches!(self.structure.terminal_morphism, TerminalSpec::Universal)
144            && self.structure.symmetry
145    }
146
147    /// Returns true if this category is linear (no weakening, no contraction).
148    pub fn is_linear(&self) -> bool {
149        matches!(self.structure.diagonal, DiagonalSpec::None)
150            && matches!(self.structure.terminal_morphism, TerminalSpec::None)
151    }
152
153    /// Returns true if this category is affine (weakening but no contraction).
154    pub fn is_affine(&self) -> bool {
155        matches!(self.structure.diagonal, DiagonalSpec::None)
156            && matches!(self.structure.terminal_morphism, TerminalSpec::Universal)
157    }
158
159    /// Returns true if this category is relevant (contraction but no weakening).
160    pub fn is_relevant(&self) -> bool {
161        matches!(self.structure.diagonal, DiagonalSpec::Universal)
162            && matches!(self.structure.terminal_morphism, TerminalSpec::None)
163    }
164}
csw_core/category.rs

csw_core/
category.rs
