Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The vocabulary in plain terms

panproto uses mathematical terms to distinguish operations that ordinary migration vocabulary often groups together. This page gives working translations and points to the chapters that define the terms more precisely.

Prerequisites: familiarity with schemas and data migration. This page also supports the intermediate route in the explanation reading guide.

Terms

panproto saysWorking meaningNearby familiar concept
protocolA registered schema language, including the names of its schema and instance theories and its structural rulesAn entry in a format registry, such as JSON Schema, Protobuf, or SQL DDL
theory (GAT)A specification of the sorts, operations, and equations used to describe a family of structuresA typed algebraic signature with laws
schemaA schema document parsed into panproto’s common representationAn api.yaml or .proto file
instanceData interpreted under a schemaA row or JSON document
vertex / edgeA schema type and a directed field or relation between typesNodes and arrows in a schema diagram
migration (morphism)A map from source schema elements to target schema elements, with optional value transformsThe structural part of a migration plan
liftApplying a compiled migration to dataRunning a data conversion; the concrete function determines its behavior
restrictIn lift_wtype, lift_functor, and schema lift --direction restrict, forwarding only the source fragment that survives in the targetA filtered source-to-target projection; this API name does not mean categorical
In panproto_inst::adjunction, reindexing a target instance back to the source of Precomposition, with direction
In panproto_inst::adjunction, carrying a source instance forward to the targetA left Kan extension, with direction
lensA forward transformation that returns a view and a complement, paired with reconstruction from that view and complementA bidirectional converter with explicit saved state
complementInformation retained during the forward transformation so that reconstruction can restore itAn undo record
round-trip laws (GetPut, PutGet, PutPut)Equations relating forward transformation and reconstructionProperties checked on concrete inputs or generated test cases
protolensA composable description from which a lens can be instantiated for matching schemasA schema-indexed transformation template
dependent opticA protolens step whose applicability depends on schema structureA template operation with a structural precondition
colimitA construction that combines theories along explicitly shared partsGluing typed specifications over a common interface
pushoutA colimit that combines two objects receiving maps from a common objectThe categorical shape associated with a structural three-way merge
existence checkA finite validation that a proposed migration covers the required casesA static precondition check rather than execution on sample data

Tutorials chiefly use schema, migration, lens, and complement. How-to guides also refer to protocols and protolenses. Remaining terms appear in the explanation chapters where their distinctions affect an operation. The glossary provides shorter formal definitions, while Schemas as theories and Migrations as morphisms develop the central representations.

See also