Related work
panproto uses generalized algebraic theory presentations, schema maps, lens complements, and source-layout records. This chapter identifies the papers associated with those components and states where the implementation is narrower than the cited construction.
The comparisons are deliberately local. A shared categorical construction or round-trip law does not make two systems equivalent, and the implementation often checks a narrower property than the surrounding mathematical literature studies.
Schemas as theories
Generalized algebraic theories (GATs) provide the formal setting for dependent sorts, operations, and equations [Cartmell (1978); Cartmell (1986)]. The panproto-gat crate implements these ingredients as Sort, Operation, Equation, and Theory, with type checking for terms and equations. Its dependent SortExpr can apply a sort to argument terms. This is the concrete sense in which panproto uses GATs.
Categorical database work supplies two related accounts of schemas and instances. Spivak treats a schema as a category and an instance as a set-valued functor (Spivak 2012). Schultz and Wisnesky instead present database schemas and instances through equational theories, with the longer mathematical development given by Schultz and colleagues [Schultz & Wisnesky (2017); Schultz et al. (2017)]. Attributed C-sets develop functorial data structures for scientific computing (Patterson et al. 2022), while Lu studies several database models through a thin-category construction (Lu 2025). These systems establish useful points of comparison for schemas-as-mathematics, but their instance categories and migration operations should not be identified with panproto’s merely from the shared vocabulary.
The binary panproto-gat::colimit function combines two Theory values over explicit legs from a shared theory. It implements an amalgamated union, including compatible same-name identification outside the shared image, and rejects non-injective legs rather than constructing their quotient. pushout_by_name constructs identity-on-name legs before calling this function. Theory assembly by colimits has a longer history in the Clear specification language and in institutions [Burstall & Goguen (1977); Burstall & Goguen (1980); Goguen & Burstall (1992); Sannella & Tarlecki (2012)]. The repository does not define or verify an institution for its GAT representation.
Ologs provide another categorical account of labeled knowledge structures (Spivak and Kent 2012). panproto schemas also have named vertices and edges, but their labels are checked against protocol and schema structures rather than interpreted as the natural-language boxes and arrows of an olog. The resemblance is representational, not an implemented translation.
Protocol definitions in panproto-protocols are Rust values built from the GAT API. The catalog thus demonstrates that the same engine can host many theory presentations. The code does not construct one global theory automatically merely because those definitions coexist; callers must supply the diagram or shared theory used by colimit, colimit_by_name, or pushout_by_name. Composing protocols by colimit describes those operations in detail.
Bidirectional transformations
Bidirectional-transformation work includes asymmetric lenses, which pair a forward view function with an update function and impose round-trip laws (Foster et al. 2007), and relational lenses, which adapt that account to database views (Bohannon et al. 2006). The constant-complement view-update account preserves information outside a view (Bancilhon and Spyratos 1981), and symmetric lenses use complements to mediate updates between peers (Hofmann et al. 2011). Edit lenses instead model changes through edit monoids and actions (Hofmann et al. 2012), while delta lenses propagate changes rather than replacement states [Diskin et al. (2011); Pacheco et al. (2012)].
The panproto-lens crate implements an asymmetric get and put over WInstance values. get returns a view and a Complement; put uses both to reconstruct a source. The law helpers compare instances structurally, and check_optic_laws exercises the obligations available for a concrete lens and instance. These checks apply to their supplied cases. They do not prove the laws for every possible instance.
Profunctor optics organize lenses, prisms, traversals, and related optics by the structure required of the carrier [Pickering et al. (2017); Clarke et al. (2024)]. Dependent optics extend the account to indexed settings (Vertechi 2023). panproto’s OpticKind uses the familiar names Iso, Lens, Prism, Affine, and Traversal, but its classifier inspects TheoryTransform variants. A scoped transform is refined from its schema edge kind: item or items yields a traversal carrier, variant yields a prism carrier, and other edges use a lens carrier. This is a structural classifier, not an implementation of the indexed-category construction in the cited dependent-optics work; corresponding optic laws require a separate concrete check.
Point-free and delta-lens calculi study algebraic composition and calculation principles for bidirectional programs [Pacheco & Cunha (2011); Pacheco et al. (2012)]. ProtolensChain also composes transformations, and it offers fused and sequential instantiation. That shared concern does not establish an equivalence between its Rust representation and either calculus. The chain tests and check_optic_laws, rather than a transfer theorem from the cited calculi, determine which properties panproto currently checks.
Cambria organizes schema versions as a graph connected by bidirectional lenses [Litt et al. (2020); Litt et al. (2021)]. panproto likewise composes migrations and complements, though its schema nodes, migration representation, and storage layer are defined independently in the panproto-mig, panproto-lens, and panproto-vcs crates. Cambria is consequently relevant to the schema-version graph pattern without serving as a specification for those modules.
Format-preserving parse and emit
Format-preserving transformation has both lens-based and grammar-based precedents. Augeas applies lenses to configuration files (Lutterkort 2008). Boomerang adds resource-sensitive alignment to a lens language, and quotient lenses reason modulo selected equivalences [Bohannon et al. (2008); Foster et al. (2008)]. BiYacc derives a parser and reflective printer from a bidirectional grammar (Zhu et al. 2015). Token-origin tracking offers a different reconstruction method for preserving layout during tree transformation (Jonge and Visser 2012), while resugaring work studies when an expanded program can recover surface syntax (Pombrio and Krishnamurthi 2014).
panproto starts from tree-sitter grammars rather than a bidirectional grammar language (Brunsfeld 2018). The parse walker stores byte spans, interstitial text, literal values, and choice evidence as schema constraints. emit_pretty either replays a subtree whose fragments tile its span or walks grammar.json to produce canonical source. decorate renders an abstract schema and parses the rendered bytes to recover a fresh layout enrichment.
The implementation thus combines ideas that the cited systems separate: grammar-directed construction, stored source fragments, and complement-like metadata. Its guarantees remain those of its own tests. A verified corpus case must reach an emission fixed point and preserve vertex-kind and edge-shape multisets; byte equality with the original source is not part of that oracle. Direct fragment replay can be byte-exact when the recorded fragments completely tile the source span.
Structured version control
Patch theory supplies categorical accounts of files, edits, and merge. Mimram and Di Giusto model patches and study pushout-based reconciliation (Mimram and Giusto 2013). Homotopical patch theory places patch laws in a higher-dimensional setting (Angiuli et al. 2014), and Darcs provides an earlier algebra of patches in a working version-control system (Roundy 2005). These works motivate the use of spans, cocones, and universal properties when discussing merge.
The panproto-vcs merge implementation is a structural three-way merge over Schema fields. It computes diffs from a base to two branches, accepts compatible one-sided changes, and records typed conflicts for incompatible changes. It also computes a theory-level pullback overlap and stores the result as diagnostic metadata. The field merge does not use that overlap to make its decisions. A failed pullback is retained as diagnostic data and does not masquerade as an empty overlap.
After the caller supplies a resolution for every conflict, verify_pushout checks totality of both vertex maps, coverage of merged vertices, survival of retained base vertices, and cocone agreement on vertices and mapped base edges. Despite its name, this function checks necessary cocone conditions rather than the full universal property. verify_pushout_universal constructs and checks a unique mediator only on vertices; its documentation defers edge-level factorization. The code thus supports a delimited pushout account, not a proof that every merge result is a pushout in the full schema category.
Content addressing comes from the Merkle-tree and git traditions [Merkle (1988); Chacon & Straub (2014)]. CommitObject stores a schema-tree identifier, parent commits, an optional migration, protocol metadata, data-set identifiers, migration-complement identifiers, edit logs, theory identifiers, and CST-complement identifiers. The object store has distinct variants for data sets, migration complements, and CST complements. These fields are independently addressable objects linked by a commit; the code does not collapse them into a single four-field mathematical object.
Database schema-evolution systems provide a more operational comparison. PRISM associates schema modification operators with forward and backward dependencies for data and query migration (Curino et al. 2008). panproto’s existence checking, compilation, lifting, and inversion cover related questions for its Migration type, but neither the available operators nor their inverse classifications are identical to PRISM’s. In particular, CoercionClass classifies individual coercion witnesses as Iso, Retraction, Projection, or Opaque; it is not a reimplementation of PRISM’s operator table.
Conflict-free replicated data types guarantee convergence by constraining replicated operations (Shapiro et al. 2011). panproto-vcs instead computes a repository merge and may return conflicts requiring a resolution. The APIs solve different coordination problems, so convergence properties from CRDTs do not transfer to the VCS merge.
Cross-schema translation
Data exchange studies mappings between source and target schemas, universal solutions, cores, and the chase (Fagin et al. 2005). Work on composition shows why a mapping language may need second-order tuple-generating dependencies to remain closed under composition (Fagin et al. 2005). CQL develops migrations in an algebraic database setting [Schultz & Wisnesky (2017); Schultz et al. (2017)]. These results help distinguish existence, construction, composition, and information loss. panproto does not expose universal solutions or second-order tgds as aliases for its lens chains, and CoercionClass does not decide whether a target instance is a core.
The panproto-mig pipeline checks migration existence, compiles surviving vertices and edges, lifts instances, composes migrations, and inverts bijective migrations. Its hom_search API treats schema matching as an optimization problem. find_span can return a partial overlap, while find_morphisms and find_best_morphism restrict the same search to total morphisms. The current edge map sends each source edge to one target edge. It cannot map an edge to a longer path or express a one-to-many field correspondence, a limit documented on FoundMorphism.
Systems such as Apache Calcite separate a common relational representation from backend adapters (Begoli et al. 2018). panproto also separates protocol-specific definitions from shared algorithms, but its common values are schemas, theories, migrations, and instances rather than query plans. The adapter analogy describes software organization only; the repository does not implement Calcite’s relational algebra, optimizer rules, or calling conventions.