Lenses

A lens is a function-like object that maps between two Model classes. didactic ships three subtypes, in increasing strictness:

type shape round-trip law
Mapping[A, B] A -> B none; one-way
Lens[A, B] A -> (B, complement) and (B, complement) -> A GetPut and PutGet
Iso[A, B] A -> B and B -> A total bijection

Defining an Iso

import didactic.api as dx


class FirstLast(dx.Model):
    given: str
    family: str


class LastFirst(dx.Model):
    family: str
    given: str


class SwapNameOrder(dx.Iso[FirstLast, LastFirst]):
    def forward(self, n: FirstLast) -> LastFirst:
        return LastFirst(family=n.family, given=n.given)

    def backward(self, n: LastFirst) -> FirstLast:
        return FirstLast(given=n.given, family=n.family)


iso = SwapNameOrder()
iso(FirstLast(given="Ada", family="Lovelace"))
# LastFirst(family='Lovelace', given='Ada')

The Iso is also callable: iso(x) is iso.forward(x).

Defining a Lens

For a transformation that loses information in the forward direction but stores enough on the side to recover it:

class WithComment(dx.Model):
    payload: str
    comment: str


class WithoutComment(dx.Model):
    payload: str


class StripComment(dx.Lens[WithComment, WithoutComment]):
    def forward(self, w: WithComment) -> tuple[WithoutComment, str]:
        return WithoutComment(payload=w.payload), w.comment

    def backward(self, view: WithoutComment, comment: str) -> WithComment:
        return WithComment(payload=view.payload, comment=comment)

Composing lenses

>> composes by chaining forward and backward through both lenses:

ab >> bc        # Lens[A, C]

Composition is associative; identity is the trivial Iso.

Verifying lens laws

dx.testing.verify_iso runs the iso round-trip law on Hypothesis samples:

from hypothesis import strategies as st

dx.testing.verify_iso(
    SwapNameOrder(),
    st.builds(FirstLast, given=st.text(), family=st.text()),
)

For a non-iso lens, use check_lens_laws which runs GetPut. The complementary helpers verify_mapping, verify_lens_composition, verify_iso_inverse, and verify_migration_round_trip cover the rest of the algebraic laws.

Schema-parametric lenses

For a lens family that operates on many concrete schemas (Avro to OpenAPI conversion, for instance), use didactic.api.DependentLens. It wraps panproto's ProtolensChain and produces a concrete Lens once instantiated against a pair of schemas. See the reference page for the full surface.

A chain can be authored declaratively in the panproto-lens-dsl surface (JSON, YAML, or Nickel) and loaded through DependentLens.from_dsl_path (extension-dispatched) or the format-specific from_dsl_json, from_dsl_yaml, and from_dsl_nickel classmethods. Each loader takes the document source plus the entry vertex of the source schema the chain is anchored against.

Correspondence discovery

When you have two concrete schemas and don't yet know how their vertices line up, find_correspondences enumerates the structure-preserving vertex maps between them via panproto's hom search, scored by alignment quality; best_correspondence returns just the top match. The discovered Correspondence.vertex_map feeds DependentLens.auto_generate_with_hints directly, giving a discover-then-derive pipeline:

import didactic.api as dx

best = dx.best_correspondence(src_schema, tgt_schema)
if best is not None and best.quality >= 0.8:
    chain = dx.DependentLens.auto_generate_with_hints(
        src_schema,
        tgt_schema,
        protocol,
        best.vertex_map,
    )

Known pairings can be pinned with anchors; injective, surjective, or bijective maps can be required with monic, epic, and iso. Note that the schemas didactic builds from Model classes are single-vertex (their structure lives in the Theory), so the search is informative on multi-vertex schemas: protocol schemas built by hand and schemas recovered by didactic.codegen.source.parse.