Explanation
These chapters explain the representations and checks that underlie panproto. They assume that you can read a schema and a structural diff, but they do not assume category theory. Procedures belong in the how-to guides, while interface details belong in the reference.
Schemas, migrations, and lenses
Begin with What panproto solves, and consult The vocabulary in plain terms when an unfamiliar term appears. Schemas as theories first describes the common representation used for different protocols. Migrations as morphisms then explains a migration and the operations that move data along it. Search may return a partial correspondence as a span. Together, these chapters supply the background needed by the tutorials and most how-to guides.
When a conversion discards information or must support updates in both directions, continue from the glossary definition of a lens to Lenses and round-trip laws. What panproto verifies distinguishes runtime validation and test evidence from properties that the implementation assumes.
Search, composition, and version control
Searching for a morphism describes how panproto searches for a partial or total schema correspondence. Alignment evidence explains how names, types, and other evidence affect that search.
Composing protocols by colimit concerns the colimit construction used to describe protocol structure. Schema version control semantics concerns structural changes to concrete schemas and their histories. The two chapters use related categorical constructions at different levels of the system.
Layout enrichment and Source-code emission address parsing, canonical emission, and preservation of source layout. Architecture identifies the crates that implement these operations and the data that crosses their boundaries.
Denotational semantics
The denotational semantics chapters specify the expression language, both DSLs, protolens composition, merge, and the theory REPL. Begin with Shared notation; the remaining chapters assume familiarity with typed abstract syntax, inference rules, and elementary category theory.
Related work locates these constructions in the literature. It is best read after the chapters on schemas, migrations, and lenses.
Chapter map
| Question | Read |
|---|---|
| What problem and vocabulary do I need? | What panproto solves, then The vocabulary in plain terms |
| How are schemas and migrations represented? | Schemas as theories, then Migrations as morphisms |
| How does automatic correspondence work? | Searching for a morphism, then Alignment evidence |
| What makes a migration bidirectional? | Lenses and round-trip laws |
| How are protocols or branches combined? | Composing protocols by colimit, then Schema version control semantics |
| How does source-code round-tripping work? | Layout enrichment, then Source-code emission |
| Which claims are mechanically checked? | What panproto verifies |
| Where does the implementation live? | Architecture |