panproto-gat 0.5.0

GAT (Generalized Algebraic Theory) engine for panproto
Documentation

panproto-gat

Generalized Algebraic Theory (GAT) engine for panproto.

This is Level 0 of the panproto architecture -- the only component implemented directly in Rust rather than as data. It provides the foundational type system for defining schema languages: sorts, operations, equations, and theories, along with morphisms and colimits (pushouts) for composing them.

API

Item Description
Theory Named collection of sorts, operations, and equations
resolve_theory Resolve a theory by name from a registry
Sort / SortParam Dependent type declarations
Operation Term constructor with typed inputs and outputs
Equation / Term Judgemental equalities between terms
TheoryMorphism Structure-preserving map between theories
check_morphism Validate that a morphism is well-formed
colimit Compute pushouts of theories for composition
Model / ModelValue Interpretations of theories in Set
migrate_model Transport a model along a morphism
GatError Error type for GAT operations

Example

use panproto_gat::{Theory, Sort, Operation};

let mut theory = Theory::new("SimpleGraph");
theory.add_sort(Sort::new("V"));
theory.add_sort(Sort::new("E"));
theory.add_op(Operation::new("src", vec!["E"], "V"));
theory.add_op(Operation::new("tgt", vec!["E"], "V"));

License

MIT