Lens DSL: denotational semantics

In plain terms

A lens DSL spec is a recipe for building a bidirectional transform between two schemas. You declare which fields map to which (with optional value-level expressions), and the compiler produces a triple of functions that satisfies three round-trip laws by construction. This page pins down what the spec compiles to and what “satisfies the laws” means.

Surface syntax

The Nickel surface (canonical authoring form). JSON and YAML surfaces are isomorphic via serde.

{
  id = "user.v3-to-v4",
  description = "Rename `name` and replace `age` with `years`",
  source = "dev.example.user.v3",
  target = "dev.example.user.v4",
  steps = [
    { rename_field = { old = "name", new = "display_name" } },
    { remove_field = "age" },
    { add_field = { name = "years", kind = "integer", default = 0, expr = "old.age" } },
  ],
}

Each step is a single-key object whose key selects the variant. The full step grammar is in crates/panproto-lens-dsl/src/document.rs.

Abstract syntax

pub struct LensDocument {
    pub id: String,
    pub description: String,
    pub source: String,
    pub target: String,

    // Body: exactly one of the six variants is present.
    pub steps:     Option<Vec<Step>>,
    pub rules:     Option<Vec<Rule>>,
    pub compose:   Option<ComposeSpec>,
    pub auto:      Option<AutoSpec>,
    pub from_diff: Option<FromDiffSpec>,
    pub symmetric: Option<SymmetricSpec>,

    // Modifier: oriented rewrites appended to the compiled chain.
    pub directed_equations: Option<Vec<DirectedEquationSpec>>,

    // Rule-variant metadata.
    pub passthrough: Option<Passthrough>,
    pub invertible:  Option<bool>,

    // Protocol-specific extension metadata.
    pub extensions: HashMap<String, serde_json::Value>,
}

pub enum Step {
    // High-level field combinators
    RemoveField { remove_field: String },
    RenameField { rename_field: RenameSpec },
    AddField    { add_field: AddFieldSpec },

    // Value-level transforms
    ApplyExpr    { apply_expr: ApplyExprSpec },
    ComputeField { compute_field: ComputeFieldSpec },

    // Structural combinators
    HoistField { hoist_field: HoistSpec },
    NestField  { nest_field: NestSpec },
    Scoped     { scoped: ScopedSpec },
    Pullback   { pullback: PullbackSpec },

    // Sort-level coercions and merges
    CoerceSort { coerce_sort: CoerceSortSpec },
    MergeSorts { merge_sorts: MergeSortsSpec },

    // Elementary theory operations
    AddSort      { add_sort: AddSortSpec },
    DropSort     { drop_sort: String },
    RenameSort   { rename_sort: RenameSpec },
    AddOp        { add_op: AddOpSpec },
    DropOp       { drop_op: String },
    RenameOp     { rename_op: RenameSpec },
    AddEquation  { add_equation: EquationSpec },
    DropEquation { drop_equation: String },
}

The top-level type is LensDocument, not LensSpec. The document carries source and target NSID fields naming the two schemas and exactly one body variant: steps, rules, compose, symmetric, auto, or from_diff. A directed_equations modifier may accompany a body, appending oriented rewrites to the compiled chain.

Compilation has two entry points. compile is schema-independent: it handles the schema-parametric bodies (steps, rules, compose, symmetric) and rejects auto and from_diff, which need a concrete source and target schema, with LensDslError::AutoRequiresSchemas. compile_with_schemas handles those two as well, running the auto-generation engine for auto and diff_to_protolens for from_diff. It also verifies the compiled chain against the declared target: the chain is instantiated at the source schema and the NSID of its output schema is compared against target, yielding LensDslError::TargetMismatch on divergence. The schema-independent path cannot run that comparison, since it has no schema to instantiate against.

Semantic domain

For schemas $S$, $V$ and complement type $C$, the set of lenses on $(S,V,C)$ is

$$\mathsf{Lens}(S,V,C)=(S\to V)\times (S\times V\times C\to S)\times (S\to C)$$

with elements written as triples $(\mathsf{get},\mathsf{put},\mathsf{complement})$. The implementation in panproto-lens represents this triple by the Lens struct; the categorical model is the standard asymmetric-lens construction of Foster et al. (2007) with complements after Litt et al. (2020). The semantic function

$$[[\cdot ]]:\mathsf{LensDocument}\to \mathsf{Sch}\to \mathsf{Lens}$$

takes a document and a source schema and returns a concrete lens. (The target schema and the complement type are determined by the document and the source.)

The three laws

A lens $l=(\mathsf{get},\mathsf{put},\mathsf{complement})$ is lawful iff for all $s\in S$ and $v\in V$:

$$\text{GetPut:}\mathsf{put}(s,\mathsf{get}(s),\mathsf{complement}(s))=s$$

$$\text{PutGet:}\mathsf{get}(\mathsf{put}(s,v,c))=v$$

$$\text{PutPut:}\mathsf{put}(\mathsf{put}(s,v_1,c),v_2,c)=\mathsf{put}(s,v_2,c)$$

panproto_lens::laws::check_get_put, check_put_get, and check_put_put are deterministic runtime checkers: each takes a lens and a given instance, derives the views and complements it needs from that instance ($check\_put\_get$ perturbs a single leaf value; $check\_put\_put$ reuses one complement on both puts), and asserts the corresponding equation.

Semantic equations

For each step constructor, $[[\cdot ]]$ is a function $\mathsf{Step}\to \mathsf{Sch}\to \mathsf{Protolens}$, where a $\mathsf{Protolens}$ is a schema-parameterised lens (see Protolens composition). The document-level semantics is the left-to-right composition of the per-step semantics, applied to the source schema:

$$[[\mathsf{LensDocument}(\mathsf{id}=d,\mathsf{steps}=[s_1,\dots ,s_k])]]S=[[s_k]]S_{k-1};\cdots ;[[s_1]]S_0$$

where $S_0=S$ and $S_i=\mathsf{target}([[s_i]]S_{i-1})$. The composition operator $;$ is the sequential lens composition

$$\begin{array}{rl}{\mathsf{get}}_{l_1;l_2}(s)& ={\mathsf{get}}_{l_2}({\mathsf{get}}_{l_1}(s))\\ {\mathsf{complement}}_{l_1;l_2}(s)& =({\mathsf{complement}}_{l_1}(s),{\mathsf{complement}}_{l_2}({\mathsf{get}}_{l_1}(s)))\\ {\mathsf{put}}_{l_1;l_2}(s,v,(c_1,c_2))& ={\mathsf{put}}_{l_1}(s,{\mathsf{put}}_{l_2}({\mathsf{get}}_{l_1}(s),v,c_2),c_1)\end{array}$$

For a representative subset of steps:

$$\begin{array}{rl}[[\mathsf{RemoveField}\{f\}]]S& ={\mathsf{drop}}_f(\mathsf{get}={\mathsf{forget}}_f,\mathsf{complement}={\mathsf{capture}}_f,\mathsf{put}={\mathsf{restore}}_f)\\ [[\mathsf{RenameField}\{f\mapsto g\}]]S& =(\mathsf{get}={\mathsf{rename}}_{f\mapsto g},\mathsf{complement}=\epsilon ,\mathsf{put}={\mathsf{rename}}_{g\mapsto f})\\ [[\mathsf{AddField}\{f,d\}]]S& =(\mathsf{get}={\mathsf{insert}}_{f,d},\mathsf{complement}=\epsilon ,\mathsf{put}={\mathsf{forget}}_f)\\ [[\mathsf{ApplyExpr}\{e_{\to },e_{\leftarrow }\}]]S& =(\mathsf{get}=[[e_{\to }]],\mathsf{complement}=\mathsf{snapshot},\mathsf{put}=[[e_{\leftarrow }]])\end{array}$$

where $\epsilon$ is the trivial complement (a singleton) and $[[\cdot ]]$ on the right-hand side of $\mathsf{ApplyExpr}$ is the expression-language semantics. The remaining 15 step constructors follow the same pattern; the implementation of each lives under crates/panproto-lens-dsl/src/steps.

Composition between adjacent step semantics is gated at construction time by protolens_composable: see Protolens composition. Compilation in the implementation is handled by panproto_lens_dsl::compile, which produces a CompiledLens carrying the ProtolensChain corresponding to $[[\cdot ]]S$ along with the value-level FieldTransforms extracted from any $\mathsf{ApplyExpr}$ steps.

Complement composition

Sequential composition of lenses requires composing their complements. Complement::compose is a partial commutative monoid:

• Identity. The empty complement $\epsilon$ satisfies $\epsilon \cdot c=c\cdot \epsilon =c$.
• Commutativity. When defined, $c_1\cdot c_2=c_2\cdot c_1$.
• Associativity. When defined, $(c_1\cdot c_2)\cdot c_3=c_1\cdot (c_2\cdot c_3)$.
• Partiality: $c_1\cdot c_2$ is defined iff:
  • $c_1$ and $c_2$ have the same source-schema fingerprint (otherwise ComplementFingerprintMismatch); and
  • For every key $k$ in both, $c_1(k)=c_2(k)$ (otherwise ComplementConflict with the offending key).

Pre-flight predicate: Complement::is_compatible(c1, c2).

The fingerprint is a 64-bit hash of the source schema (computed with the standard library’s DefaultHasher in panproto_lens::asymmetric::schema_fingerprint), so complements computed against syntactically distinct but structurally equal schemas are still compatible.

Soundness

The compilation function preserves lawfulness: if every step compiles to a lawful lens (which the combinator algebra guarantees), the composed result is lawful. The checks that back this are sampled, not exhaustive. The property tests in crates/panproto-lens/src/laws.rs run GetPut, PutGet, and PutPut over generated scenarios that span the identity and projection families, nested trees of depth three, lenses carrying vertex and edge remaps, and field-transform lenses, with the PutGet and PutPut views drawn from a view-mutation strategy rather than a single canned perturbation. The DSL side adds crates/panproto-lens-dsl/tests/step_laws.rs, which compiles a document per step constructor and runs the same runtime law checks on the instantiated chain. A coerce_sort step (and each directed_equations entry) is checked for honesty when the DSL compiles it: the declared coercion class’s round-trip laws are run against sampled inputs of the source kind, and a class that fails on those samples is refused with LensDslError::CoercionNotHonest. Each of these is evidence, not proof; the samples that were tried do not certify a law for inputs that were not.

The runtime checkers above remain deterministic smoke checks: they assert each law of a supplied lens on one instance, and they are not the sampling layer.

What is intentionally not modelled

• Lossy migrations as full lenses. A migration that drops information cannot satisfy GetPut. The DSL allows DropField, but the resulting object is a partial lens; the laws hold only on the surviving structure, and CI tests skip the GetPut law for steps annotated as lossy.
• Time complexity of put. Some combinators have linear put cost in the size of the source; the semantics fixes the value, not the cost.
• Equivalence of two distinct DSL specs that compile to the same lens. The DSL deliberately exposes step ordering even when steps commute; canonicalisation is left to the user.

See also

• Reference: lens combinators for the combinator algebra.
• How-to: write lenses in the lens DSL.
• Lenses and round-trip laws (plain-terms version).
• Protolens composition for schema-parameterised lenses.
• Foster et al. (2007) and Litt et al. (2020).