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 four variants is present.
    pub steps:   Option<Vec<Step>>,
    pub rules:   Option<Vec<Rule>>,
    pub compose: Option<ComposeSpec>,
    pub auto:    Option<AutoSpec>,

    // 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, or auto). The resolver loads the source schema and the compiler applies the body to it, then checks that the result matches the named target. See panproto_lens_dsl::compile.

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 property-test runners that sample $s$, $v$, $v_1$, $v_2$ from the schema’s value space and assert each 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. Property tests in crates/panproto-lens/src/laws.rs verify each combinator against random inputs sampled from the schema’s value space.

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).