Pith. sign in

REVIEW 4 major objections 5 minor 27 references

Categories of tagged lenses

T0 review · 4 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The paper proves that tagged lenses form a strict symmetric monoidal category, with a strict monoidal functor into the category of putget lenses; two additional tag laws independently force getput and putput.

desk verdict A genuinely new formalization of lens-law entailment via tags, with correct getput/putput proofs, but the central categorical claims are uncheckable because the appendix diagrams are corrupted and no algebraic composite-tag formula is given. read the letter →

arxiv 2607.25706 v1 pith:VF6LYNXC submitted 2026-07-28 math.CT

Matt Wilson This is my paper · ORCID
classification math.CT MSC 18M05
keywords taggedlenseslenslawsputgetvery-well-behavedcartesianmonoidalcategoriessymmetricchange-dependingtagsfirst-last-depending
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Tagged lenses are a formal way to add side-effect counters to very-well-behaved lenses. The paper shows that whenever such a tag commutes with the lens's update operation, the induced lens automatically satisfies the putget law, and the tagged lenses themselves form a strict symmetric monoidal category. The induced-lens construction is then a strict monoidal functor into the category of putget lenses. Two additional design laws for tags—recording only genuine changes, or recording only first and last values—are shown to be compositional and to force the getput and putput laws respectively. Together these results give a categorical explanation of why relaxed lens laws can be understood through tag behaviour.

What carries the argument

The central object is a tag, a morphism $T: S \times V \times V \to S$ recording a side effect indexed by the prior and future view values. The defining axiom requires the tag to commute with the underlying put: $\mathrm{put}(T(s,v_1,v_2),v_3) = T(\mathrm{put}(s,v_3),v_1,v_2)$, which also forces $g(T(s,v_1,v_2)) = g(s)$. From a tagged lens the induced put is $P(s,v) = \mathrm{put}(T(s,g(s),v),v)$. Two tag laws carry the argument: change-dependence $T(s,v,v)=\mathrm{id}$ makes trivial updates invisible, and first-last dependence $T(T(s,v,v'),v',v'')=T(s,v,v'')$ collapses intermediate updates. The composition rule for tags is chosen so that $L$ is functorial, and the proofs use string diagrams for cartesian monoidal categories.

What would settle it

Checking in small finite sets whether every tuple satisfying the tag commutation axiom yields $g(\mathrm{put}(T(s,g(s),v),v)) = v$ would settle Proposition 1; finding a single counterexample, or a composed tag that fails the commutation law, would refute the category and functor claims.

Watch

Extended reading notes

Core claim

The central claim is that for every cartesian monoidal category $\mathbb{C}$, tagged vwb-lenses form a strict symmetric monoidal category $\mathrm{TL}(\mathbb{C})$, and the construction sending a tagged lens $(\mathrm{put}, g, T)$ to the putget lens with put $P(s,v) = \mathrm{put}(T(s,g(s),v),v)$ is a strict symmetric monoidal, injective-on-objects functor $L: \mathrm{TL}(\mathbb{C}) \to \mathrm{pgL}(\mathbb{C})$. The same construction guarantees putget for every tagged lens. If the tag is change-depending ($T(s,v,v)=\mathrm{id}$), the induced lens additionally satisfies getput; if the tag is first-last-depending ($T(T(s,v,v'),v',v'')=T(s,v,v'')$), it additionally satisfies putput; a tag satisfying both induces a very-well-behaved lens. The paper's examples—counters, flags, and scaled views—are all recovered as induced lenses of such tags.

Load-bearing premise

All results collapse if the requirement that a tag commute with the underlying put—$\mathrm{put}(T(s,v_1,v_2),v_3) = T(\mathrm{put}(s,v_3),v_1,v_2)$—is not the right way to model side effects, since the putget proof and the composition rule both depend on it.

Editorial extensions

If this is right

  • Every tagged lens induces a putget lens, so tagged updates compose exactly as putget lenses compose, with the induced put factoring through the tag.
  • A change-depending tag is enough to upgrade putget to well-behaved: the induced lens satisfies getput.
  • A first-last-depending tag is enough to force putput, and combining both tag laws yields a very-well-behaved lens.
  • The subcategories of change-depending and first-last-depending tagged lenses are themselves symmetric monoidal, giving a chain of embeddings from tagged lenses down to vwb lenses.
  • Known examples like counters that record only changes, flags, and scaled views are unified as induced lenses of tags, with their lens laws following from the two tag laws rather than ad hoc checks.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the tag commutation axiom is the exact condition separating putget from the other lens laws, then relaxing or generalising that axiom should produce a taxonomy of partial lens-law entailments; the paper does not explore this.
  • The two tag laws could be tested for independence: since each forces a distinct lens law, a tag satisfying neither should induce a lens satisfying only putget, and the examples suggest such tags exist.
  • The construction is stated for cartesian monoidal categories; a natural extension would be to replace the copying and deletion structure by a non-cartesian monoidal structure, where the string-diagram proofs would need to be reworked.
  • Because composition, unitality, and associativity of tags all reduce to the same commutation axiom, any collection of putget lenses admitting a coherent tag assignment would automatically form a subcategory of $\mathrm{pgL}(\mathbb{C})$, suggesting a route to classifying which putget subcategories arise from tags.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper introduces "tagged lenses": a vwb lens (get, put) equipped with a tag T:S×V×V→S satisfying the commutation law put(T(s,v1,v2),v3)=T(put(s,v3),v1,v2). Each tagged lens induces an ordinary lens P(s,v)=put(T(s,g(s),v),v). The paper proves that every induced lens satisfies putget, that change-depending tags (T(s,v,v)=s) force getput, and that first-last-depending tags (T(T(s,v,v'),v',v'')=T(s,v,v'')) force putput. It further claims that tagged lenses form a strict symmetric monoidal category TL(C), that change-depending and first-last-depending tags define symmetric monoidal subcategories, and that the induced-lens construction is a strict monoidal injective-on-objects functor L:TL(C)→pgL(C). The main text gives algebraic proofs for the getput entailment; the categorical and closure claims are relegated to diagrammatic appendix proofs.

Significance. If the categorical claims are correct, the paper gives a clean, elementary demonstration that lens laws can be entailed compositionally by simple side-effect laws, and the change-dependence/first-last-dependence distinction is a genuinely useful organising idea. The algebraic getput argument in Proposition 6 is correct: P(s,g(s))=put(T(s,g(s),g(s)),g(s))=put(s,g(s))=s. The putput argument in Proposition 7 also checks out algebraically when the tag commutation law and the underlying putput law are used. The examples are well chosen and illustrate the intended phenomena. However, the central category and functor claims (Propositions 2, 3, and 5) are not verifiable from the submitted text because their proofs are sequences of string-diagram equalities that are largely unreadable in the provided rendering, and no algebraic formula for the composite tag is supplied. This is a load-bearing gap that must be fixed before the paper can be accepted.

major comments (4)
  1. [§4 and Appendix A] The sequential composition of tags is defined only by a string diagram; no pointwise or point-free algebraic formula for the composite tag T_comp is given. The proof of Proposition 2 then consists of a long chain of diagram equalities that are not legible in the submitted rendering: boxes and wires are misaligned, and several steps appear to duplicate or drop components. Since the tag commutation law is exactly what makes TL(C) a category, the existence of the category is not checkable as written. Please give an explicit algebraic definition of T_comp and a readable proof that it satisfies Definition 2.
  2. [Appendix C] Proposition 3, the strict monoidal functoriality of L:TL(C)→pgL(C), is proved only by diagrammatic equalities. The text says the composite tag is chosen so that L(ϕ2∘ϕ1)=L(ϕ2)∘L(ϕ1), but the proof that this equality holds with the displayed T_comp is unreadable. This is the second load-bearing claim of the paper. Please provide a direct algebraic verification of L(ϕ2∘ϕ1)=L(ϕ2)∘L(ϕ1), and similarly for the monoidal coherence.
  3. [Appendix D] The proof that first-last-depending tags are closed under sequential composition is again a long diagrammatic equality sequence and is not legible in the submitted text. This closure is needed for Proposition 5, i.e., for fldepTL(C) to be a subcategory. Since the paper's advertised contribution is compositional entailment, this closure proof must be checkable; please supply an algebraic proof.
  4. [Definition 2] The tag commutation law put(T(s,v1,v2),v3)=T(put(s,v3),v1,v2) is load-bearing: it is used in the proof that g∘T is trivial and in the putput argument, and the category TL(C) exists only if the composite tag again satisfies it. The paper does not explain why this specific law is the natural or minimal axiom. Please add a short discussion of the choice, ideally showing how the law is preserved by the composite-tag construction rather than merely asserting it.
minor comments (5)
  1. [Abstract and §1] The abstract contains "definetagged" with a missing space; throughout the paper there are similar spacing issues, e.g., "set-basedlenses" and "definetagged vwb-lenses".
  2. [Examples 3–7] Examples 3, 4, 5, 6, and 7 each repeat the sentence "Note that PutCount satisfies putget..." even when the example is not PutCount; this is confusing and should be corrected so each example reports its own laws.
  3. [Example 7 and Example 10] There is an inconsistency in the PutScaled example: Example 7 defines put((x,y),v)=(v,vy/x), while Example 10 defines the underlying put as ↑((x,y),v)=(v,y) and the tag as Scale((x,y),v,v')=(x,v'y/v). These formulas do not agree; please fix the typo and make the example self-consistent.
  4. [§2.2 and Appendix B] The string-diagram notation is introduced only informally, and the appendix refers to colours ("orange", "green") that are not present in the monochrome rendering, making the intended picture impossible to reconstruct. Either include properly typeset coloured diagrams or replace the colour references with explicit wire labels.
  5. [Appendix A] The associativity proof contains an equality that appears to switch the order of T2 and T1 without comment and several steps where wires labelled ↑1, ↑2, g2, g3 are duplicated or dropped. If these are rendering artifacts, the source should be recompiled; otherwise the proof step is unjustified.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: tag laws are genuine hypotheses, and the induced-lens theorems are derived from them rather than assumed.

full rationale

The derivation chain is self-contained. Definition 2 imposes the tag commutation law as a hypothesis, and Definition 3 defines the induced lens; Proposition 1 then derives putget from the underlying vwb putget law. The tag axiom is stronger than needed for putget, but it is not a restatement of the conclusion, so this is not circular. In Section 4 the authors explicitly say there are many ways to compose tags and they choose the one for which L is functorial; this is an openly stated construction or ansatz, not a hidden derivation, so it does not amount to circularity. Propositions 6 and 7 derive getput and putput from the change-depending and first-last-depending hypotheses; those hypotheses are not equivalent to the conclusions (for example, PutFlag satisfies putput via a first-last tag while PutCountChanges satisfies getput via a change-depending tag), and the proofs use the stated tag laws together with the vwb laws. No parameters are fitted to data and no empirical prediction is made. The main caveat is verifiability: several appendix proofs are sequences of corrupted or hard-to-read string diagrams (notably the proof of Proposition 8 that the composite tag satisfies the commutation law, and the functoriality proof in Proposition 9), so the central claims are difficult to check from the submitted text. That is a correctness or reproducibility concern, not circularity. The self-citations in the references are contextual related-work citations and are not load-bearing for the main theorems.

Assumptions & free parameters 0 free parameters · 4 assumptions · 1 invented entities

The central construction rests on the new tag axiom (commutation with put), the assumption that the underlying lens is vwb, and the standard structure of cartesian monoidal categories. No numerical parameters are fitted. The only invented entity is the tag itself, which is motivated by but not independently evidenced by prior examples.

assumptions (4)
  • standard math Every object of C has a cartesian comonoid structure (copy and delete maps), and every morphism is a comonoid homomorphism.
    Used throughout Section 2.2 to present lenses and tags as string diagrams; this is the standard structure of cartesian monoidal categories.
  • domain assumption The underlying lens (put, get) in any tagged lens is very-well-behaved (Definition 1).
    Definition 2 begins with '(put, g) is a vwb lens from V to S'; the induced-lens laws for the tagged lens inherit the putget, getput, and putput laws of this base lens.
  • ad hoc to paper Tags satisfy the commutation law put(T(s,v1,v2),v3) = T(put(s,v3),v1,v2).
    Definition 2 introduces this as the defining tag axiom. It is the load-bearing premise that makes the induced lens satisfy putget and makes tag composition coherent. The paper motivates it by the demand that tags have no effect on the view, but the commutation with put is a new postulate.
  • domain assumption Change-depending tags satisfy T(s,v,v)=s, and first-last-depending tags satisfy T(T(s,v,v'),v',v'')=T(s,v,v'').
    Section 5 defines these as the two compositional design laws for tags; the paper proves they are preserved under composition and entail getput and putput respectively.
invented entities (1)
  • tag: a morphism T: S×V×V → S in a cartesian monoidal category
    purpose: Models a side-effect applied during put, parameterized by the old and new view values; the tag is the auxiliary data forgotten by the induced lens functor L.
    The tag is the paper's new object of study. It is anchored to previously known lenses (PutCountChanges, PutFlag, PutScaled) from [11,19], which are shown to admit tagged presentations, but the paper offers no falsifiable prediction outside the framework itself.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Categories of tagged lenses." pith.science (2026). https://pith.science/paper/VF6LYNXC

@misc{pith2026260725706,
  author       = {Pith},
  title        = {Pith review of: Categories of tagged lenses},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/VF6LYNXC}},
  note         = {Machine review of arXiv:2607.25706}
}
read the original abstract

To better understand the landscape of well-behavedness laws for lenses on strict Cartesian symmetric monoidal categories, we define tagged lenses. We prove that tagged lenses form a strict symmetric monoidal category equipped with a strict symmetric monoidal functor into the category of putget lenses. We then observe compositional entailment for the other two lens laws, identifying change-dependence and first-last dependence of tags as sufficient conditions for getput and putput, respectively.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 20 canonical work pages

  1. [1]

    Notions of bidirectional computation and entangled state monads.Mathematics of Program Construction, page 187–214, 2015.doi:10.1007/978-3-319-19797-5-9

    Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, and Perdita Stevens. Notions of bidirectional computation and entangled state monads.Mathematics of Program Construction, page 187–214, 2015.doi:10.1007/978-3-319-19797-5-9

    work page doi:10.1007/978-3-319-19797-5-9 2015

  2. [2]

    Reflections on monadic lenses.Lecture Notes in Computer Science, page 1–31, 2016.doi: 10.1007/978-3-319-30936-1-1

    Faris Abou-Saleh, James Cheney, Jeremy Gibbons, James McKinna, and Perdita Stevens. Reflections on monadic lenses.Lecture Notes in Computer Science, page 1–31, 2016.doi: 10.1007/978-3-319-30936-1-1

    work page doi:10.1007/978-3-319-30936-1-1 2016

  3. [3]

    Compositional game theory, compositionally.Electronic Proceedings in Theoretical Computer Science, 333:198–214, Feb 2021

    Robert Atkey, Bruno Gavranović, Neil Ghani, Clemens Kupke, Jérémy Ledent, and Fredrik Nordvall Forsberg. Compositional game theory, compositionally.Electronic Proceedings in Theoretical Computer Science, 333:198–214, Feb 2021. URL:http://dx.doi.org/10. 4204/EPTCS.333.14,doi:10.4204/eptcs.333.14

    work page doi:10.4204/eptcs.333.14 2021

  4. [4]

    Bancilhon and N

    F. Bancilhon and N. Spyratos. Update semantics of relational views.ACM Transactions on Database Systems, 6(4):557–575, December 1981.doi:10.1145/319628.319634

    work page arXiv 1981

  5. [6]

    Fibre optics

    Dylan Braithwaite, Matteo Capucci, Bruno Gavranović, Jules Hedges, and Eigil Fjeldgren Rischel. Fibre optics, 2021.arXiv:2112.11145

    work page Pith review arXiv 2021

  6. [7]

    Higher lenses

    Paolo Capriotti, Nils Anders Danielsson, and Andrea Vezzosi. Higher lenses. In2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1–13, 2021. doi:10.1109/LICS52264.2021.9470613

    arXiv 2021

  7. [8]

    Translating Extensive Form Games to Open Games with Agency

    Matteo Capucci, Neil Ghani, Jérémy Ledent, and Fredrik Nordvall Forsberg. Translating extensive form games to open games with agency, 2021.arXiv:2105.06763. 12

    work page Pith review arXiv 2021

  8. [9]

    A diagrammatic approach to symmetric lenses.Electronic Proceedings in Theoretical Computer Science, 333:79–91, Feb 2021

    Bryce Clarke. A diagrammatic approach to symmetric lenses.Electronic Proceedings in Theoretical Computer Science, 333:79–91, Feb 2021. URL:http://dx.doi.org/10.4204/ EPTCS.333.6,doi:10.4204/eptcs.333.6

    work page doi:10.4204/eptcs.333.6 2021

Show all 27 references
  1. [10]

    Profunctor optics, a categorical update, 2020.arXiv:2001

    Bryce Clarke, Derek Elkins, Jeremy Gibbons, Fosco Loregian, Bartosz Milewski, Emily Pillmore, and Mario Román. Profunctor optics, a categorical update, 2020.arXiv:2001. 07488

    2020

  2. [11]

    A clear picture of lens laws

    Sebastian Fischer, Zhenjiang Hu, and Hugo Pacheco. A clear picture of lens laws. In Ralf Hinze and Janis Voigtländer, editors,Mathematics of Program Construction, pages 215–223, Cham, 2015. Springer International Publishing

    2015

  3. [12]

    Nathan Foster, Michael B

    J. Nathan Foster, Michael B. Greenwald, Jonathan T. Moore, Benjamin C. Pierce, and Alan Schmitt. Combinators for bi-directional tree transformations: A linguistic approach to the view update problem. In Jens Palsberg and Martín Abadi, editors,Proceedings of the 32nd ACM SIGPLA...

    2005

  4. [13]

    Categories of semantic concepts, 2020

    James Hefford, Vincent Wang, and Matthew Wilson. Categories of semantic concepts, 2020. arXiv:2004.10741

    2020 arXiv

  5. [14]

    Heunen and J

    C. Heunen and J. Vicary.Categories for Quantum Theory: An Introduction. Oxford Graduate Texts in Mathematics Series. Oxford University Press, 2019.doi:10.1093/oso/ 9780198739623.001.0001

    2019 doi

  6. [15]

    Double categories of open dynamical systems (extended abstract)

    David Jaz Myers. Double categories of open dynamical systems (extended abstract). Electronic Proceedings in Theoretical Computer Science, 333:154–167, Feb 2021. URL: http://dx.doi.org/10.4204/EPTCS.333.11,doi:10.4204/eptcs.333.11

    2021 doi

  7. [16]

    Lens put-put laws: monotonic and mixed.Elec- tronic Communications of the EASST, 49, 2012

    Michael Johnson and Robert Rosebrugh. Lens put-put laws: monotonic and mixed.Elec- tronic Communications of the EASST, 49, 2012. Version archived for private and non- commercial use with the permission of the author/s and according to publisher conditions. For further rights p...

    2012 doi

  8. [17]

    Games on graphs: a compositional approach, 2020.arXiv:2006.03493

    Elena Di Lavore, Jules Hedges, and Paweł Sobociński. Games on graphs: a compositional approach, 2020.arXiv:2006.03493

    2020 arXiv

  9. [18]

    Springer-Verlag, New York,

    Saunders MacLane.Categories for the Working Mathematician. Springer-Verlag, New York,

  10. [19]

    A tangled web of 12 lens laws

    Keisuke Nakano. A tangled web of 12 lens laws. In Shigeru Yamashita and Tetsuo Yokoy- ama, editors,Reversible Computation, pages 185–203, Cham, 2021. Springer International Publishing

    2021

  11. [20]

    Monadic combinators for "putback" style bidirectional programming

    Hugo Pacheco, Zhenjiang Hu, and Sebastian Fischer. Monadic combinators for "putback" style bidirectional programming. InProceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and Program Manipulation, PEPM ’14, page 39–50, New York, NY, USA, 2014. Association for C...

    2014

  12. [21]

    Categories of optics.arXiv: Category Theory, 2018

    Mitchell Riley. Categories of optics.arXiv: Category Theory, 2018

    2018

  13. [22]

    David I. Spivak. Generalized lens categories via functorsCop→Cat, 2020.arXiv:1908. 02202. 13

    2020

  14. [23]

    Cyber kittens, or some first steps towards categorical cybernetics

    Toby St Clere Smithe. Cyber kittens, or some first steps towards categorical cybernetics. Electronic Proceedings in Theoretical Computer Science, 333:108–124, Feb 2021. URL: http://dx.doi.org/10.4204/EPTCS.333.8,doi:10.4204/eptcs.333.8

    2021 doi

  15. [24]

    The safari of update structures: Visiting the lens and quantum enclosures.Electronic Proceedings in Theoretical Computer Science, 333:1–18, Feb 2021

    Matthew Wilson, James Hefford, Guillaume Boisseau, and Vincent Wang. The safari of update structures: Visiting the lens and quantum enclosures.Electronic Proceedings in Theoretical Computer Science, 333:1–18, Feb 2021. URL:http://dx.doi.org/10.4204/ EPTCS.333.1,doi:10.4204/eptcs.333.1

    2021 doi

  16. [25]

    Composing bidirectional programs monad- ically

    Li-yao Xia, Dominic Orchard, and Meng Wang. Composing bidirectional programs monad- ically. In Luís Caires, editor,Programming Languages and Systems, pages 147–175, Cham,

  17. [28]

    Springer International Publishing. A The (Symmetric Monoidal) Category of Tagged Lenses Proposition 8(The CategoryTL(C)).For every cartesian monoidal categoryCa symmetric monoidal category of tagged lensesTL(C)can be constructed with •Objects given by the objects ofC •Morphism...

  18. [1971]

    Graduate Texts in Mathematics, Vol. 5

  19. [2019]

    URL:http://arxiv.org/abs/1910.03656,arXiv:1910.03656

    1910 arXiv

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.