csw-core 0.1.0

//! Core categorical specification types.

#[cfg(feature = "serde")]
use serde::{Deserialize, Serialize};

/// A specification of categorical structure.
///
/// This is the main type representing a category with its structural features.
/// From this specification, a type system can be derived.
#[derive(Clone, Debug, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct CategorySpec {
    /// Name of the category/type system
    pub name: String,

    /// Base objects (primitive types)
    pub base_objects: Vec<BaseObject>,

    /// Structural features present in the category
    pub structure: StructuralFeatures,
}

/// A base/primitive object in the category.
///
/// These become the ground types in the derived type system.
#[derive(Clone, Debug, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct BaseObject {
    /// Name of the base type
    pub name: String,

    /// Optional description
    pub description: Option<String>,
}

/// Structural features present in a category.
///
/// These determine what type constructors and structural rules
/// will be present in the derived type system.
#[derive(Clone, Debug, Default, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct StructuralFeatures {
    // === Limits ===
    /// Terminal object (unit type, 1)
    pub terminal: bool,

    /// Binary products (pair types, A × B)
    pub products: bool,

    /// Initial object (empty type, 0)
    pub initial: bool,

    /// Binary coproducts (sum types, A + B)
    pub coproducts: bool,

    // === Closed Structure ===
    /// Exponentials (function types, A → B) - cartesian
    pub exponentials: bool,

    // === Monoidal Structure ===
    /// Tensor product specification (A ⊗ B)
    pub tensor: Option<TensorSpec>,

    /// Linear hom / internal hom (A ⊸ B)
    pub linear_hom: bool,

    // === Structural Morphisms ===
    /// Diagonal morphism availability (contraction)
    pub diagonal: DiagonalSpec,

    /// Terminal morphism availability (weakening)
    pub terminal_morphism: TerminalSpec,

    /// Symmetry/braiding (exchange rule)
    pub symmetry: bool,
}

/// Specification for monoidal tensor product.
#[derive(Clone, Debug, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub struct TensorSpec {
    /// Symbol for tensor (default: "⊗")
    pub symbol: String,

    /// Symbol for unit (default: "I")
    pub unit_symbol: String,

    /// Whether associativity is strict or weak
    pub associativity: Associativity,
}

impl Default for TensorSpec {
    fn default() -> Self {
        Self {
            symbol: "⊗".to_string(),
            unit_symbol: "I".to_string(),
            associativity: Associativity::Weak,
        }
    }
}

/// Associativity type for monoidal structure.
#[derive(Clone, Debug, Default, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum Associativity {
    /// Strict associativity: (A ⊗ B) ⊗ C = A ⊗ (B ⊗ C)
    Strict,
    /// Weak associativity: (A ⊗ B) ⊗ C ≅ A ⊗ (B ⊗ C)
    #[default]
    Weak,
}

/// Specification for diagonal morphism (contraction/copying).
#[derive(Clone, Debug, Default, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum DiagonalSpec {
    /// No diagonal (linear: cannot copy)
    #[default]
    None,
    /// Diagonal for all objects (cartesian: can always copy)
    Universal,
    /// Diagonal only for specified objects
    Restricted(Vec<String>),
}

/// Specification for terminal morphism (weakening/discarding).
#[derive(Clone, Debug, Default, PartialEq, Eq)]
#[cfg_attr(feature = "serde", derive(Serialize, Deserialize))]
pub enum TerminalSpec {
    /// No terminal morphisms (relevant: cannot discard)
    #[default]
    None,
    /// Terminal morphism for all objects (affine/cartesian: can always discard)
    Universal,
    /// Only for specified objects
    Restricted(Vec<String>),
}

impl CategorySpec {
    /// Returns true if this category has full structural rules (weakening + contraction + exchange).
    pub fn is_cartesian(&self) -> bool {
        matches!(self.structure.diagonal, DiagonalSpec::Universal)
            && matches!(self.structure.terminal_morphism, TerminalSpec::Universal)
            && self.structure.symmetry
    }

    /// Returns true if this category is linear (no weakening, no contraction).
    pub fn is_linear(&self) -> bool {
        matches!(self.structure.diagonal, DiagonalSpec::None)
            && matches!(self.structure.terminal_morphism, TerminalSpec::None)
    }

    /// Returns true if this category is affine (weakening but no contraction).
    pub fn is_affine(&self) -> bool {
        matches!(self.structure.diagonal, DiagonalSpec::None)
            && matches!(self.structure.terminal_morphism, TerminalSpec::Universal)
    }

    /// Returns true if this category is relevant (contraction but no weakening).
    pub fn is_relevant(&self) -> bool {
        matches!(self.structure.diagonal, DiagonalSpec::Universal)
            && matches!(self.structure.terminal_morphism, TerminalSpec::None)
    }
}