19  Protolens Engine

A Protolens is a reusable schema transform that produces a concrete lens for any schema meeting a precondition. Where a Lens binds to two specific schemas, a Protolens is a dependent function: given a schema \(S\) and a protocol, it yields a \(\text{Lens}(F(S), G(S))\) where \(F\) and \(G\) are schema transforms.¹

For the concrete lens primitives (get, put, complement), see Chapter 10. For the automated pipeline that derives protolens chains from schema diffs, see Chapter 20.

NoteRelationship to prior work

The term “protolens” is specific to panproto. Related ideas include:

• Cambria combinators (Litt et al. 2022): each corresponds to an elementary protolens whose source transform is identity. Protolenses generalize Cambria by adding explicit schema parameterization, precondition checking, and schema-dependent complement types. Cambria operates on implicit schemas; protolenses take the schema as an explicit argument.
• Haskell lens families (Lens s t a b): parameterized over types, not schemas. Lens families allow source/target types to differ, but complement structure doesn’t vary with the parameter.
• Delta lenses (Johnson and Rosebrugh 2013): generalize asymmetric lenses by making source and view into categories. The commutativity property of protolenses (commuting with schema migration) is the same coherence condition delta lenses formalize.

What distinguishes protolenses: schema-dependent complements, precondition diagnostics, and guaranteed commutativity with migration. See the tutorial’s protolens chapter for the full comparison.

19.1 TheoryEndofunctor and TheoryTransform

File: crates/panproto-gat/src/schema_functor.rs

A TheoryEndofunctor pairs a precondition with a schema transform:

        /// The new sort name.
        new: Arc<str>,
    },
    /// Add an operation.
    AddOp(Operation),
    /// Drop an operation and dependent equations.
    DropOp(Arc<str>),
    /// Rename an operation.
    RenameOp {

The TheoryTransform enum describes how a schema transform acts on a theory:

        to: ValueKind,
    },
    /// Theory must have a merger sort for the given kind.
    HasMerger(ValueKind),
    /// Theory must have a conflict policy with this name.
    HasPolicy(Arc<str>),
    /// Conjunction.
    All(Vec<Self>),
    /// Disjunction.
    Any(Vec<Self>),
    /// Negation.
    Not(Box<Self>),
}

/// How a theory endofunctor transforms a theory.
#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub enum TheoryTransform {
    /// Identity: T ↦ T
    Identity,
    /// Add a sort: T ↦ T + {sort}
    ///
    /// The optional `vertex_kind` specifies the schema-level vertex kind
    /// for the Grothendieck fibration. When `None`, the vertex kind is
    /// derived from the sort: `Val(vk)` → canonical value kind name,
    /// `Structural` → sort name.
    AddSort {
        /// The sort to add.
        sort: Sort,
        /// Schema-level vertex kind override.
        vertex_kind: Option<Arc<str>>,
    },
    /// Drop a sort and all dependent ops/equations.
    DropSort(Arc<str>),
    /// Rename a sort.
    RenameSort {

Each variant modifies a theory in one specific way:

Variant	Effect on theory	Inverse
Identity	No change	Self
AddSort(s)	Add sort s	DropSort(s.name)
DropSort(n)	Remove sort n and cascade to dependent ops/eqs	AddSort(...)
RenameSort{old,new}	Rename sort from old to new	RenameSort{new,old}
AddOp(op)	Add operation op	DropOp(op.name)
DropOp(n)	Remove operation n and cascade to dependent eqs	AddOp(...)
RenameOp{old,new}	Rename operation from old to new	RenameOp{new,old}
AddEquation(eq)	Add equation eq	DropEquation(eq.name)
DropEquation(n)	Remove equation n	AddEquation(...)
Pullback(morph)	Sort/op renaming induced by a morphism	(n/a)
Compose(f,g)	Apply f then g	Compose(g_inv, f_inv)
CoerceSort{sort,kind,expr}	Change sort’s value kind, install coercion expr	(n/a)
MergeSorts{a,b,merged,expr}	Merge two sorts via a merger expression	(n/a)
AddSortWithDefault{sort,expr}	Add sort with default value expression	DropSort(sort.name)
AddDirectedEquation(deq)	Add a directed equation (rewrite rule)	DropDirectedEquation(deq.name)
DropDirectedEquation(n)	Remove directed equation n	AddDirectedEquation(...)

19.1.1 Enriched transforms

Some variants carry computation:

• CoerceSort changes a sort’s value kind (e.g., string to int) and installs an expression for the coercion at migration time.
• MergeSorts combines two sorts (e.g., firstName + lastName to fullName) using a merger expression.
• AddSortWithDefault adds a sort with a default value expression for existing data.
• AddDirectedEquation / DropDirectedEquation manage rewrite rules that specify computation direction.

19.1.2 Cascading drops

DropSort cascades: removing a sort also removes all operations referencing it (as input or output) and all equations referencing those operations. DropOp similarly cascades to equations. The result is always well-formed.

        inverse_expr: Option<panproto_expr::Expr>,
        /// Round-trip classification of this coercion.
        coercion_class: CoercionClass,
    },
    /// Merge two sorts into one.
    MergeSorts {
        /// The first sort to merge.
        sort_a: Arc<str>,
        /// The second sort to merge.
        sort_b: Arc<str>,
        /// The name for the merged sort.
        merged_name: Arc<str>,
        /// The merger expression.
        merger_expr: panproto_expr::Expr,
    },
    /// Add a sort with a default expression for backward compatibility.

19.1.3 Composing schema transforms

TheoryEndofunctor::compose chains two transforms \(F\) and \(G\) into “apply \(F\), then apply \(G\)”. The precondition of the composed transform is the conjunction of the first transform’s precondition with an unconstrained placeholder for the second (the second’s precondition applies to the output of the first, which can’t be statically checked). Dynamic checking occurs at apply time.

    }
    result
}

/// Compute the set of sort names reachable from `start` via directed
/// operation edges.
///
/// An operation `op(a₁: S₁, …, aₙ: Sₙ) → T` creates directed edges
/// from each input sort Sᵢ to the output sort T. Starting from `start`,
/// we follow these directed edges to find all transitively reachable sorts.
///
/// This mirrors the schema-level BFS over outgoing edges: operations in
/// the theory correspond to edges in the schema, and the input→output
/// direction corresponds to the src→tgt direction.

19.2 TheoryConstraint: precondition predicates

A TheoryConstraint defines which theories a protolens can operate on:

#[derive(Debug, Clone, PartialEq, Eq, serde::Serialize, serde::Deserialize)]
pub enum TheoryConstraint {
    /// Any theory satisfies this.
    Unconstrained,
    /// Theory must have a sort with this name.
    HasSort(Arc<str>),
    /// Theory must have an operation with this name.
    HasOp(Arc<str>),
    /// Theory must have an equation with this name.
    HasEquation(Arc<str>),
    /// Theory must have a directed equation with this name.
    HasDirectedEq(Arc<str>),
    /// Theory must have a value sort of the given kind.
    HasValSort(ValueKind),
    /// Theory must have a coercion sort between the given kinds.
    HasCoercion {
        /// The source value kind.

The constraint language is propositional logic over structural predicates:

• HasSort(n): the theory must contain a sort named n.
• HasOp(n): the theory must contain an operation named n.
• HasEquation(n): the theory must contain an equation named n.
• All, Any, Not: standard Boolean connectives.
• Unconstrained: always satisfied.

The satisfied_by method evaluates the predicate against a concrete Theory in \(O(|C| \cdot |T|)\) time, where \(|C|\) is the constraint tree size and \(|T|\) is the number of sorts/ops/equations.

19.3 The protolens struct

File: crates/panproto-lens/src/protolens.rs

The Protolens struct bundles the source and target schema transforms with a complement constructor:

    },
}

/// A protolens: a dependent function from schemas to lenses.
///
/// A `Protolens` is **not** a lens. A [`Lens`] is a concrete pair
/// (`get`, `put`) between two fixed schemas. A `Protolens` is a
/// *function* that, given any schema satisfying its precondition,
/// *produces* a `Lens`.
///
/// ```text

Key fields:

• source: The schema transform \(F\) that produces the source schema of the instantiated lens.
• target: The schema transform \(G\) that produces the target schema.
• complement_constructor: How the complement type depends on the schema (see Section 19.8).

The applicable_to method checks whether a given schema satisfies the source transform’s precondition by converting the schema to an implicit theory (vertex kinds become sorts, edge kinds become operations) and evaluating the constraint.

19.4 Instantiation

Instantiation is the core operation: given a schema \(S\) and protocol, produce a concrete \(\text{Lens}(F(S), G(S))\).

    #[must_use]
    pub fn applicable_to(&self, schema: &Schema) -> bool {
        self.check_applicability(schema).is_ok()
    }

    /// Check applicability with failure reasons.
    ///
    /// # Errors
    ///
    /// Returns a list of human-readable reasons why the precondition
    /// is not satisfied.
    pub fn check_applicability(&self, schema: &Schema) -> Result<(), Vec<String>> {
        let constraint = SchemaConstraint::from_theory_constraint(&self.source.precondition);
        let reasons = constraint.check(schema);
        if reasons.is_empty() {
            Ok(())
        } else {
            Err(reasons)
        }
    }

    /// Instantiate this protolens at a specific schema, producing a concrete
    /// [`Lens`].
    ///
    /// This is Π-type elimination: applying the dependent function to a
    /// specific schema.
    ///
    /// # Errors
    ///
    /// Returns [`LensError::ProtolensError`] if either endofunctor's
    /// transform fails to apply.

The instantiation pipeline:

1. Compute source schema: Apply \(F\) to \(S\) via apply_theory_transform_to_schema. If \(F\) is the identity, this is a clone.
2. Compute target schema: Apply \(G\) to \(S\).
3. Derive migration: Compare \(F(S)\) and \(G(S)\) structurally to compute a CompiledMigration (surviving set, vertex remap, edge remap, resolver).
4. Return lens: Bundle the compiled migration with the source and target schemas.

The apply_theory_transform_to_schema function bridges theory-level and schema-level operations:

• RenameSort{old,new} renames vertex kinds.
• DropSort(n) removes vertices with kind n and their incident edges.
• AddSort(s) inserts a new vertex with kind s.name.
• RenameOp{old,new} renames edge kinds.
• DropOp(n) removes edges with kind n.

Note

The schema_to_implicit_theory function extracts an implicit theory from a schema: each unique vertex kind becomes a sort, and each unique edge kind becomes a unary operation. This allows protolens preconditions (which operate on Theory values) to be evaluated against schemas without requiring an explicit theory object.

19.5 Commutativity checking (order independence)

A protolens is well-behaved if instantiating at one schema and then migrating produces the same result as migrating first and then instantiating. In other words, both paths through the diagram below arrive at the same lens.²

For elementary protolens constructors in protolens::elementary, commutativity holds by construction: each constructor’s source and target transforms act locally (on a single sort or operation), so their action commutes with schema morphisms that don’t touch the affected elements. Commutativity for composed protolenses follows from commutativity of the components.

In practice, commutativity is verified by the test suite rather than checked at runtime. The ProtolensChain::instantiate method trusts that the chain was constructed from verified components.

19.6 Vertical and horizontal composition

Protolenses compose in two dimensions: chaining transforms sequentially, and combining independent transforms in parallel.

19.6.1 Vertical composition (chaining transforms)

Given a protolens from \(F\) to \(G\) and another from \(G\) to \(H\), vertical composition produces a single protolens from \(F\) to \(H\):³

                    vec![format!(
                        "None of the alternatives were satisfied: {}",
                        reasons.join("; ")
                    )]
                }
            }
            Self::Not(c) => {
                if c.satisfied_by(schema) {
                    vec![format!("Constraint should NOT be satisfied but is: {c:?}")]
                } else {
                    vec![]
                }
            }
        }
    }

    /// Lift a `TheoryConstraint` to a `SchemaConstraint`.
    #[must_use]
    pub fn from_theory_constraint(tc: &panproto_gat::TheoryConstraint) -> Self {
        match tc {
            panproto_gat::TheoryConstraint::Unconstrained => Self::Unconstrained,
            panproto_gat::TheoryConstraint::HasSort(name) => {
                Self::HasVertexKind(Name::from(&**name))

The composed protolens uses the first step’s source transform and the second step’s target transform. The complement is the composite of both complements; during get, both steps’ lost data is captured.

19.6.2 Horizontal composition (combining independent transforms)

Given two independent protolenses that operate on different parts of the theory, horizontal composition applies both simultaneously:⁴

            panproto_gat::TheoryConstraint::HasOp(name) => Self::HasEdgeKind(Name::from(&**name)),
            panproto_gat::TheoryConstraint::HasEquation(name) => Self::Theory(
                panproto_gat::TheoryConstraint::HasEquation(Arc::clone(name)),
            ),
            panproto_gat::TheoryConstraint::All(cs) => {
                Self::All(cs.iter().map(Self::from_theory_constraint).collect())
            }
            panproto_gat::TheoryConstraint::Any(cs) => {
                Self::Any(cs.iter().map(Self::from_theory_constraint).collect())
            }
            panproto_gat::TheoryConstraint::Not(c) => {
                Self::Not(Box::new(Self::from_theory_constraint(c)))
            }
            // Enriched theory constraints delegate to the theory-level checker.
            other @ (panproto_gat::TheoryConstraint::HasDirectedEq(_)
            | panproto_gat::TheoryConstraint::HasValSort(_)
            | panproto_gat::TheoryConstraint::HasCoercion { .. }
            | panproto_gat::TheoryConstraint::HasMerger(_)
            | panproto_gat::TheoryConstraint::HasPolicy(_)) => Self::Theory(other.clone()),
        }
    }
}

Horizontal composition uses TheoryEndofunctor::compose to build the composed source and target transforms.

19.6.3 ProtolensChain

The ProtolensChain struct provides a convenient wrapper for vertical composition chains:

/// Vertical composition of protolenses: given `η : F ⟹ G` and
/// `θ : G ⟹ H`, produce `θ ∘ η : F ⟹ H`.
///
/// The target endofunctor of `eta` must match the source of `theta`.
/// This is checked dynamically at instantiation time.
///
/// # Errors
///
/// Currently infallible, but returns `Result` for future compatibility
/// with static compatibility checks.
pub fn vertical_compose(eta: &Protolens, theta: &Protolens) -> Result<Protolens, LensError> {
    let complement = ComplementConstructor::Composite(vec![
        eta.complement_constructor.clone(),
        theta.complement_constructor.clone(),
    ]);

    Ok(Protolens {
        name: Name::from(format!("{}.{}", theta.name, eta.name)),
        source: eta.source.clone(),
        target: theta.target.clone(),
        complement_constructor: complement,
    })
}

/// Horizontal composition of protolenses: given `η : F ⟹ G` and
/// `θ : F' ⟹ G'`, produce `η * θ : F∘F' ⟹ G∘G'`.
///
/// # Errors
///
/// Currently infallible, but returns `Result` for future compatibility
/// with static compatibility checks.
pub fn horizontal_compose(eta: &Protolens, theta: &Protolens) -> Result<Protolens, LensError> {
    let source = eta.source.compose(&theta.source);
    let target = eta.target.compose(&theta.target);
    let complement = ComplementConstructor::Composite(vec![
        eta.complement_constructor.clone(),
        theta.complement_constructor.clone(),
    ]);

    Ok(Protolens {
        name: Name::from(format!("{}*{}", theta.name, eta.name)),
        source,
        target,
        complement_constructor: complement,
    })
}

// ---------------------------------------------------------------------------
// ProtolensChain
// ---------------------------------------------------------------------------

/// A chain of protolenses for vertical composition.
///
/// Each step's target endofunctor feeds into the next step's source.
/// Instantiating the chain at a schema produces a composed lens.
#[derive(Debug, Clone, serde::Serialize, serde::Deserialize)]
pub struct ProtolensChain {
    /// The individual protolens steps.
    pub steps: Vec<Protolens>,
}

impl ProtolensChain {
    /// Create a new chain from steps.
    #[must_use]
    pub const fn new(steps: Vec<Protolens>) -> Self {
        Self { steps }
    }

    /// Check if the chain can be instantiated at the given schema.
    ///
    /// An empty chain (identity) is applicable to any schema. Otherwise,
    /// the first step must be applicable.
    #[must_use]
    pub fn applicable_to(&self, schema: &Schema) -> bool {
        if self.steps.is_empty() {
            return true;
        }
        self.steps[0].applicable_to(schema)
    }

Instantiating a chain applies each step sequentially, using the previous step’s target schema as the next step’s input. The resulting lenses are composed via crate::compose::compose.

19.7 Elementary protolens constructors

The protolens::elementary module provides nine atomic protolens constructors, each corresponding to one TheoryTransform variant:

Constructor	Type signature	Lossless?
add_sort(name, kind, default)	\(\text{Id} \Rightarrow \text{AddSort}(\tau)\)	Yes
drop_sort(name)	\(\text{Id} \Rightarrow \text{DropSort}(\tau)\)	No
rename_sort(old, new)	\(\text{Id} \Rightarrow \text{RenameSort}(\text{old}, \text{new})\)	Yes
add_op(name, src, tgt, kind)	\(\text{Id} \Rightarrow \text{AddOp}(\text{op})\)	Yes
drop_op(name)	\(\text{Id} \Rightarrow \text{DropOp}(\text{op})\)	No
rename_op(old, new)	\(\text{Id} \Rightarrow \text{RenameOp}(\text{old}, \text{new})\)	Yes
add_equation(eq)	\(\text{Id} \Rightarrow \text{AddEquation}(\text{eq})\)	Yes
drop_equation(name)	\(\text{Id} \Rightarrow \text{DropEquation}(\text{eq})\)	Yes
pullback(morphism)	\(\text{Id} \Rightarrow \text{Pullback}(\phi)\)	Yes

All elementary constructors have identity as their source transform. Additive constructors (adding a sort/op/equation) have Unconstrained as their precondition. Subtractive or renaming constructors require the element to exist via HasSort, HasOp, or HasEquation.

For example, elementary::drop_sort constructs:

}

/// Lift a protolens along a theory morphism.
///
/// Given protolens `η` and morphism `φ : T1 → T2`, produces a protolens
/// that operates on schemas of T2 instead of T1. The endofunctors are
/// composed with the morphism's renames, and the precondition is lifted
/// (sort/op references renamed according to the morphism).
#[must_use]
pub fn lift_protolens(protolens: &Protolens, morphism: &panproto_gat::TheoryMorphism) -> Protolens {
    Protolens {
        name: Name::from(format!("{}[{}]", protolens.name, morphism.name)),
        source: lift_endofunctor(&protolens.source, morphism),
        target: lift_endofunctor(&protolens.target, morphism),
        complement_constructor: protolens.complement_constructor.clone(),
    }
}

/// Lift an entire protolens chain along a theory morphism.
#[must_use]
pub fn lift_chain(

19.8 complementconstructor as schema-dependent Type

The ComplementConstructor enum describes how the complement type depends on the schema at instantiation time:

/// How the complement type depends on the schema at instantiation time.
#[derive(Debug, Clone, Serialize, Deserialize)]
#[non_exhaustive]
pub enum ComplementConstructor {
    /// Complement is always empty (lossless protolens).
    Empty,
    /// Complement captures dropped sort data.
    DroppedSortData {
        /// The sort whose data is captured.
        sort: Name,
    },
    /// Complement captures dropped edge data.
    DroppedOpData {
        /// The operation whose data is captured.
        op: Name,
    },
    /// Complement is the kernel of a natural transformation.
    NatTransKernel {
        /// Name of the natural transformation.
        nat_trans_name: Name,
    },
    /// Forward direction requires a default for an added element.
    AddedElement {
        /// Name of the element being added.
        element_name: Name,
        /// What kind of element (e.g. `"string"`, `"record"`).
        element_kind: String,
        /// Default value to use when instantiating.
        default_value: Option<Value>,
    },
    /// Complement captures coerced sort data with a specific round-trip class.
    CoercedSortData {

This is a type-level description, not a runtime complement. At instantiation time, the constructor determines what data the resulting lens’s get direction will capture:

• Empty: lossless transformation (renames, additions, equation changes).
• DroppedSortData { sort }: the complement stores all nodes anchored at vertices with the dropped sort’s kind.
• DroppedOpData { op }: the complement stores all arcs corresponding to the dropped edge kind.
• NatTransKernel { nat_trans_name }: the complement is the kernel of the transform (used in advanced composition scenarios).
• Composite(vec): the complement is the union of multiple sub-complements, arising from vertical composition.

The is_lossless method on Protolens checks whether the complement constructor is Empty, providing a quick determination of whether round-tripping preserves all data without external storage.

19.9 Integration with the cascade module

File: crates/panproto-mig/src/cascade.rs

The protolens engine connects to panproto-mig’s morphism tower via the cascade module. The tower has three levels:

1. Theory morphism: maps sorts to sorts, operations to operations.
2. Schema morphism (induced by the theory morphism): renames vertex kinds and edge kinds.
3. Data migration (induced by the schema morphism): the CompiledMigration that transforms instances.

The induce_schema_morphism function bridges levels 1 and 2. The protolens engine adds a parallel path: instead of requiring a single theory morphism, it factors the morphism into elementary transforms via factorize (Section 20.3) and maps each factor to a protolens. This produces a ProtolensChain that, when instantiated, yields a composed Lens.

The advantage over the direct cascade path is compositionality: each protolens step is independently verifiable, and the chain can be inspected, serialized, and modified without recomputing the full migration.

19.10 Schema constraints vs Theory constraints

TheoryConstraint operates on implicit theories extracted from schemas via schema_to_implicit_theory. This extraction is lossy: vertex IDs are discarded (only kinds survive as sorts), edge names are lost (only kinds survive as operations), and structural properties like edge multiplicities and ordering constraints have no representation.

SchemaConstraint checks schemas directly, bypassing the lossy extraction. It supports predicates that TheoryConstraint can’t express:

• HasVertex(id): the schema must contain a vertex with this ID.
• HasEdgeBetween(src, tgt, kind): a specific edge must exist between two specific vertices.
• VertexCount(kind, min, max): the schema must have between min and max vertices of the given kind.

The check() method on SchemaConstraint returns a Vec<ConstraintFailure> instead of a boolean. Each failure includes the constraint that failed, the schema element it checked, and a human-readable explanation.

SchemaConstraint::from_theory_constraint bridges the two systems: it converts a TheoryConstraint into the closest SchemaConstraint equivalent by mapping HasSort(n) to “any vertex with kind n exists” and HasOp(n) to “any edge with kind n exists”. The conversion is conservative; it never accepts a schema that the original TheoryConstraint would reject.

Protolens::check_applicability uses SchemaConstraint internally and returns the full list of ConstraintFailure values, giving callers actionable diagnostics instead of a bare boolean.

19.11 Endofunctor fusion

The fuse() method on ProtolensChain composes all steps’ target transforms into a single TheoryTransform::Compose tree. For a chain with steps \([F_1, F_2, \ldots, F_n]\), fusion produces a single Protolens whose target transform is \(\text{Compose}(F_1, \text{Compose}(F_2, \ldots \text{Compose}(F_{n-1}, F_n)))\).

The fused protolens requires a single instantiate call, which applies the composed transform to the input schema once. Without fusion, ProtolensChain::instantiate applies each step sequentially, materializing \(n-1\) intermediate schemas. For a chain of length \(n\) with schemas of size \(|S|\), fusion reduces instantiation from \(O(n \cdot |S|^2)\) to \(O(|S|^2)\) (one migration derivation instead of \(n\)).

Complement constructors from all steps merge into a Composite variant, preserving the per-step complement structure for accurate round-trip data capture.

ProtolensChain::instantiate calls fuse() automatically. Calling fuse() explicitly is useful for serializing the composed protolens or inspecting the transform tree.

19.12 Functorial lifting

lift_protolens transforms a protolens defined over one protocol’s theories into an equivalent protolens over another protocol’s theories, given a theory morphism between the two protocols.

The implementation has three components:

1. lift_endofunctor: Given a TheoryEndofunctor \(F\) and a morphism \(\phi : T_1 \to T_2\), produce a new endofunctor \(\phi^* F\) that acts on \(T_2\)-theories. The target transform is composed with Pullback($\phi$): first pull back the schema along the morphism, then apply the original transform, then push forward. The precondition is lifted by renaming sort and operation references through \(\phi\)’s maps.

2. lift_constraint: Rename sort and operation references in a TheoryConstraint (or SchemaConstraint) via the morphism’s sort map and op map. HasSort("Vertex") becomes HasSort($\phi$.sort_map["Vertex"]).

3. lift_protolens: Lift both the source and target endofunctors, preserving the complement constructor. A DroppedSortData { sort: "Vertex" } becomes DroppedSortData { sort: $\phi$.sort_map["Vertex"] }.

lift_chain applies lift_protolens to each step in a ProtolensChain.

Categorically, lifting is precomposition with a morphism. A protolens \(\eta : F \Rightarrow G\) over theory \(T_1\) lifts to \(\phi^* \eta : \phi^* F \Rightarrow \phi^* G\) over theory \(T_2\), where \(\phi^*\) denotes pullback along \(\phi\). The naturality of \(\eta\) is preserved by the functoriality of \(\phi^*\).

19.13 Performance

Operation	Complexity	Notes
TheoryConstraint::satisfied_by	\(O(\lvert C\rvert \cdot \lvert T\rvert)\)	\(C\) = constraint tree, \(T\) = theory size
TheoryTransform::apply	\(O(\lvert T\rvert)\)	Linear scan of sorts/ops/eqs
Protolens::instantiate	\(O(\lvert S\rvert^2)\)	Schema comparison for migration derivation
ProtolensChain::instantiate	\(O(n \cdot \lvert S\rvert^2)\)	\(n\) = chain length
factorize (morphism decomposition)	\(O(\lvert\text{sorts}\rvert + \lvert\text{ops}\rvert)\)	Linear in domain/codomain sizes
Vertical composition	\(O(1)\)	Structural only, no computation
Horizontal composition	\(O(1)\)	Structural only, no computation

For typical schemas (10 to 100 vertices), instantiation completes in microseconds. The dominant cost is the migration derivation in compute_migration_between, which performs a nested scan over unmapped vertices for kind-based matching. For schemas with many vertices of the same kind, this quadratic term can become significant, but panproto schemas rarely exceed a few hundred vertices.

Composition (both vertical and horizontal) is \(O(1)\) because it only wraps the operands in new structs; no computation occurs until instantiation. This makes it cheap to build complex protolens chains speculatively and discard them if the preconditions aren’t met.

Cartmell, John. 1986. “Generalised Algebraic Theories and Contextual Categories.” Annals of Pure and Applied Logic 32: 209–43. https://doi.org/10.1016/0168-0072(86)90053-9.

Johnson, Michael, and Robert Rosebrugh. 2013. “Delta Lenses and Opfibrations.” Proceedings of the 2nd International Workshop on Bidirectional Transformations (BX 2013), Electronic communications of the EASST, vol. 57. https://doi.org/10.14279/tuj.eceasst.57.875.

Litt, Geoffrey, Martin Kleppmann, and Marc Shapiro. 2022. Project Cambria: Schema Evolution for CRDTs. Ink & Switch research essay. https://www.inkandswitch.com/cambria/.

---

1. A protolens is a reusable lens template parameterized by a schema. Given any schema meeting a precondition, it produces a concrete lens with concrete get/put operations. The formal type, \(\Pi(S : \mathsf{Schema} \mid P(S)). \mathsf{Lens}(F(S), G(S))\), captures this: \(S\) ranges over schemas satisfying predicate \(P\), and \(F\), \(G\) are schema transforms that produce the source and target of the resulting lens. In categorical literature, this is a natural transformation between theory endofunctors (Cartmell 1986).

2. Order independence means: instantiate-then-migrate produces the same result as migrate-then-instantiate. In categorical literature, this is the naturality condition for natural transformations. Given a schema morphism \(\phi : S_1 \to S_2\), the equation \(\eta_{S_2} \circ F(\phi) = G(\phi) \circ \eta_{S_1}\) must hold.

3. Chaining two protolenses: the first transforms \(F\) to \(G\), the second transforms \(G\) to \(H\), producing a single protolens from \(F\) to \(H\). In categorical notation, this is the vertical composite \(\theta \circ \eta : F \Rightarrow H\).

4. Two independent transforms are applied in parallel: one changes sorts/ops in one region of the theory, the other changes a different region. In categorical notation, this is the whiskering product \(\eta * \theta : F \circ F' \Rightarrow G \circ G'\).