Denotational semantics
This cluster pins panproto’s three DSLs and two structural constructions to a precise mathematical specification. Each page opens with an “In plain terms” section and then proceeds through a six-step skeleton:
- Surface syntax. BNF for what a user types.
- Abstract syntax. The Rust enum the parser produces.
- Semantic domain. The mathematical universe the syntax interprets into.
- Interpretation function. A semantic function defined by structural recursion on the abstract syntax, in the Scott-Strachey idiom. Typing is presented separately as an inductive relation ; evaluation is not a relation.
- Soundness. Statement of what the implementation guarantees, and which property tests or runtime checks enforce it.
- What is intentionally not modelled. The boundary of the formal account.
The pages in turn:
| Page | What it pins down |
|---|---|
| Shared notation | The judgement forms, environments, and meta-notation used across the others. Read this first. |
| Expression language | panproto-expr: terms, types, total evaluation under a step budget. |
| Lens DSL | panproto-lens-dsl: the lens triple (get, put, complement), the three round-trip laws, complement composition as a partial commutative monoid. |
| Theory DSL | panproto-theory-dsl: GAT presentations, sort/operation/equation judgements, the colimit interpretation. |
| Pushouts and merge | The pushout construction in the category of GATs, the universal property, and what the implementation verifies. |
| Protolens composition | Protolenses as natural transformations between schema endofunctors, the structural-equality criterion for composition, sequential vs fused instantiation. |
| REPL command language | panproto-repl: state model, command interpretation, and the bare-term typecheck path. |
The cluster is meant to be read by anyone who wants to know exactly what panproto guarantees. Familiarity with category theory helps but is not required: every page restates its formal content in plain terms before invoking it.