Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry beauty bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory history homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab nonassociative noncommutative noncommutative-geometry number-theory object of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    There’s a first stab at it.

    v1, current

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    Judging by Prop 3.1 of Lenses, fibrations and universal translations, lenses are just algebras for our possibility monad, at necessity and possibility.

    • CommentRowNumber3.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    It seems the terminology isn’t fixed, so I added a noted about ’well-behaved’ lenses.

    diff, v2, current

    • CommentRowNumber4.
    • CommentAuthorspitters
    • CommentTimeSep 24th 2018

    I’m told this is good. But I don’t have access at the moment: https://dl.acm.org/citation.cfm?doid=3191697.3191718

    Lenses for philosophers

    and of course we should cite the paper by Mitchell that started the discussion.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018
    • (edited Sep 24th 2018)

    Given

    necessity comonad : possibility monad = jet comonad : infinitesimal disk bundle monad,

    and since lens (in computer science) (at least lawlike ones) seem to be algebras for the possibility monad, what are algebras for the infinitesimal disk bundle?

    We’d need, EE over XX and a map T infX× XEE/XT_{inf} X \times_X E \to E/X.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 24th 2018

    Oh, is it just the constants E=K×XE = K \times X. But then what’s that exciting about lenses?

    That paper Lenses, fibrations and universal translations continues that when the VV of views is such that V1V \to 1 is split epi then a lens just is a projection.

    So people look at more general situations?

  1. Optic_C

    Ammar Husain

    diff, v8, current

    • CommentRowNumber8.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 23rd 2020

    Added a reference to a talk.

    diff, v11, current

    • CommentRowNumber9.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 27th 2021

    Added a new article

    diff, v12, current

    • CommentRowNumber10.
    • CommentAuthorDavid_Corfield
    • CommentTimeJan 27th 2021

    Another one

    diff, v13, current

    • CommentRowNumber11.
    • CommentAuthorBryceClarke
    • CommentTimeJul 4th 2021
    • (edited Jul 4th 2021)

    Added a paragraph in Generalizations about delta lenses which are a direct generalization of lenses satisfying laws. Also mentioned update-update lenses defined by Ahman-Uustalu, which are equivalent to cofunctors. Added four additional references to recent papers by Spivak, Johnson-Rosebrugh, Ahman-Uustalu, and myself.

    I hope to come back and add more recent references, as well as add further generalizations including symmetric lenses.

    diff, v14, current

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 4th 2021
    • (edited Jul 4th 2021)

    Thanks for the additions, Bryce. You’ll see that itex oddly renders adjacent letters wrongly, so instead of gsgs you need gsg s, using a space between the letters.

    At some point I should get a clearer understanding of what these devices are for.

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJul 4th 2021

    At some point I should get a clearer understanding of what these devices are for.

    Me, too. Ideally a perusal of the Idea-sections of this and related entries would clarify it. Currently it remains a little murky.

    • CommentRowNumber14.
    • CommentAuthormattecapu
    • CommentTimeJul 4th 2021

    Added a mention of lenses for systems theory

    Matteo Capucci

    diff, v15, current

    • CommentRowNumber15.
    • CommentAuthormattecapu
    • CommentTimeJul 4th 2021

    Cleaned definition a bit, added composition. Removed last paragraph about optics since it doesn’t make clear the way they represent a generalization over lenses. I’ll try to add back the content to ’optic (in computer science)’

    Matteo Capucci

    diff, v16, current

    • CommentRowNumber16.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 5th 2021

    Re #13 and the meaning of lenses, perhaps David Spivak’s comparison of them to bundles (here) is useful.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2021

    Thanks for this pointer to Spivak 19! I have now read through it and found it useful.

    But in that note, he is effectively saying that lenses are but a weird way to talk about a small fragment of (the categorical semantics of) dependent type theory.

    Strong criticism of the concept of lenses on slide 14 (p. 62 of 144):

    kinda weird [][\ldots] quite floppy [][\ldots] Totally not functorial, anything goes.

    People use lens laws to try to mitigate the floppiness [][\ldots] The lens laws are too strong, but without them lenses are too floppy.

    Quite a devastating assessment.

    Then his proposed rectification of the situation is insightful. But let’s see what the proposal really is: He speaks of “bundles” and uses fiber bundles as motivation and for illustration, but the local triviality condition on a fiber bundle is decidedly not part of the story here: His “bundles” are “display maps”.

    This becomes fully manifest on slide 22, p. 95 of 144, where he asks

    What do we really need to create a lens-like world?

    and his answer is effectively: a hyperdoctrine of dependent types!

    Moreover, he explains, the lenses are but the “in-dependent” types among these dependent types (i.e. those whose display maps are trivial as bundles).

    I admit that this one talk note by David Spivak is the only account of lenses that I have really read so far. But if this is anything to go by, then lenses are a red herring and people should be looking to dependent type theory and/or its categorical semantics.

    • CommentRowNumber18.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 5th 2021

    Which he’s looking at in that blog post I mentioned. Again the extra cases of his jump monad seem to concern fragments of dependent type theory.

    • CommentRowNumber19.
    • CommentAuthorBryceClarke
    • CommentTimeJul 5th 2021

    There is a recent blog post by Jules Hedges which discusses “dependent lenses”, which are essentially what David Spivak is introducing in those slides. Basically, a dependent lens should be thought of as a morphism between polynomial functors which are “one variable”.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2021
    • (edited Jul 5th 2021)

    I have added the following paragraph to the Idea-section:

    An insightful explanation and critique of the concept of “lenses” is offered in Spivak ACT19, where it is argued that the notion may and should be regarded as a small fragment (namely that of trivial display maps) of the general notion of (categorical semantics for) dependent types, such as discussed at hyperdoctrine and related entries.

    diff, v18, current

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2021
    • (edited Jul 5th 2021)

    By the way, it’s a bit sad that the entry lens (computer science) doesn’t even define the morphisms between lenses. Maybe whoever thinks about making any further addition to the discussion of lenses/optics on the nnLab should first take 10 minutes to bring this central entry here into some minimum shape. (Myself, I really need to look into something else now…)

    • CommentRowNumber22.
    • CommentAuthormattecapu
    • CommentTimeJul 5th 2021
    It's worth to mention here that Spivak's direction is quite novel, in FP world lenses are usually generalised to optics, i.e. certain Tambara modules.
    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2021

    Now I’d be interested in seeing Spivak critique the notion of “optic”. ;-) Did he write about it?

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeJul 5th 2021

    One way to think about it is this:

    Do we expect that the established vocabulary of category theory/type theory is incomplete? Do we expect that there are fundamental notions still to be formulated?

    I’d expect that the answer is clearly No. While I can’t prove this, it means that if somebody comes along and initiates an industry on a seemingly new abstract category-theoretic concept not seen before, some sceptical care may be needed to avoid that the wheels be re-invented, and maybe not fully roundly shaped.

    Indeed, the time-honored way to “apply category theory” goes the other way around: Instead of proliferating concept formation, one finds ever more ways of understanding the ever growing plethora of concepts that people invent as all being examples of a small number of universal constructions in category theory. Everything is a Kan extension, etc., whence the infamous phrase of “An X is just a B in C!” where “X” is from a plethora of concepts that people invent, while “B” is a basic concept of category theory, and “C” is the ambient category.

    That’s what Spivak did here to lens theory: “A lens is just a trivial display map.”

    • CommentRowNumber25.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 6th 2021

    Since we have just gained a new contributor in Bryce, who is a really nice guy, can we not just dump on the topic of his contributions?

    whence the infamous phrase of “An X is just a B in C!” …. That’s what Spivak did here to lens theory: “A lens is just a trivial display map.”

    It is all well and good in hindsight, but as you said on Twitter, Urs, the idea seems obvious in hindsight, but the process of arriving at it, especially in the context of the messy world of professional programmers and computer language designers, is non-trivial. And it goes the other way: to encourage the uptake of category-theoretic framework here, we don’t want another “A monad is a just a monoid in the category of endofunctors” moment. This is applied mathematics, and the proponents of the abstract picture need to phrase things in a way that makes sense for people at the coal-face, for whom a monoid is a scary object. Forget about “display maps” in a blah-category.

    Personally, I find the emergence of cofunctors really intriguing, they are not what one would expect coming from pure category theory. And we can get to the point of including all the information on the page, including morphisms of lenses, when we get there. We all have unfinished pages lying around, and Bryce seems keen to contribute, so I don’t think the page is going to stay incomplete (which is, of course, the permanent state of the whole nLab!) for long.

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2021

    Not sure what #25 is about – I am not reacting to anything Bryce said or wrote, nor have I even followed that.

    Instead, I am reacting to the observation in #12, #13 that our entry didn’t explain the Idea of lenses, and then to mattecapu in #22 seemingly suggesting that Spivak’s take on it is not so relevant. I explained why it looks squarely relevant to me, and I stand by that.

    (It seems a weird suggestion to me that the objective clarification of a topic on the nnLab should be conditioned on whether a basic category-theoretic term might “scare” a reader.)

    If anyone likes to lay out why Spivak’s POV on lenses is suboptimal and write a paragraph of an Idea-section for us on what they think the good perspective on lenses really is, I’d appreciate it and will read it with interest. Any such conceptual discussion – either way – is currently missing in our nnLab entries (and in related entries on “optics in computer science”).

    • CommentRowNumber27.
    • CommentAuthormattecapu
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    mattecapu in #22 seemingly suggesting that Spivak’s take on it is not so relevant.

    If this is what I communicated, I apologise, since that’s not my opinion. His is certainly an important and far-reaching realization!

    What I’m saying is, it doesn’t tell the full story. There’s a whole different direction of what it means to be a lens (arguably, a more natural one from the point of view of who created lenses in the first place) that Spivak’s generalisation misses. At least there’s an attitude to the concept of lens which can’t be reduced to ’a small fragment […] of the general notion of (categorical semantics for) dependent types’.

    Also why go all the way to dependent types? Spivak’s proposed generalisation only needs an indexed category to work, no hyperdoctrinal facilities needed.

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2021

    Might you have the energy to write a paragraph explaining “what it means to be a lens”, to you?

    • CommentRowNumber29.
    • CommentAuthormattecapu
    • CommentTimeJul 6th 2021

    Regarding morphisms of lenses (and optics): they are the morphisms in their respective categories.

    Of course one can come up with a ’2’-categorical augmentation. One direction is Myers and Spivak’s notion of ’charts’ between lenses which turns lenses into double category. Another is that of parametrised optics. A third is given by making the coend defining optics into a 2-coend, thereby turning the quotient into a groupoid.

    I might write about this in the coming days.

    • CommentRowNumber30.
    • CommentAuthorBryceClarke
    • CommentTimeJul 6th 2021

    There have been many interesting perspectives shared in this discussion, and I don’t have the energy to reply to them all. However, let me instead share some semblance of a plan for future improvements I hope to make to this page.

    • Add a Properties section which includes statements such as “lenses as algebras for a monad” and “lenses as algebras for a comonad” together with proof sketches and references for these results.

    • Perhaps a section titled “Categories of lenses” with two subsections titled Lenses as objects (where we look at lenses over a base and morphisms between them) and Lenses as morphisms where we can put the current material on the category Lens(C)Lens(\mathbf{C}).

    • Break the Generalizations section into two subsections titled Lenses without laws and Lenses with laws. These are both two very important threads, yet are quite different in flavour. For instance, Spivak’s generalisation, lenses in monoidal categories, bimorphic lenses, and optics all fall into the former category, while delta lenses, cofunctors, c-lenses (or split opfibrations) all fall into the latter.

    • Reorganise the references section, provide a short synopsis of each of the items, possibly separate into published papers and more informal work like blog posts and talk slides.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2021

    Thanks. Just to highlight that the question we bystanders have is more conceptual than technical: We are wondering: Why is the definition of lenses what it is? Why is it necessary to consider this definition? What is it good for? Why should one care?

    (If we reject Spivak’s answer as inadequate, then I really don’t know the answer to these questions and would like to know.)

    What might help is the statement of some property/theorem that holds for lenses, and then a list of examples that shows that this property/theorem subsumes a bunch of specific phenomena that arise in application or that are otherwise known to be relevant.

    • CommentRowNumber32.
    • CommentAuthormattecapu
    • CommentTimeJul 6th 2021

    @BryceClarke that’s a very good plan!

    Might you have the energy to write a paragraph explaining “what it means to be a lens”, to you?

    Yes, I will. There’s already a bit of this in under ’Idea’, I’ll expand it. I’ll probably split it between this page and ’optic’, since not everything I say might be appropriate for vanilla lenses.

    • CommentRowNumber33.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    My outsider perspective is that the definition is like it is, because this is something that comes from functional programming and is really a nitty-gritty implementation thing, not necessarily just pure theory that happens to be nice. It’s like worrying about implementation details of a real-world type theory-based proof assistant, rather than just saying “it’s all just MLTT, what’s the matter?”

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeJul 6th 2021

    David, I wonder if you think about the implications of what you are saying in #25 and #33. Essentially you are claiming in #33 that lenses are not a theoretically worthwhile concept, and in #25 that those who publish about the subject are feeble applied mathematicians who must be protected from being confronted with their proper theoretical discussion. You probably mean to do good, but it seems counterproductive.

    I was happy to learn from Spivak that lenses are but trivial dependent types, because that immediately gives them a strong theoretical status that immediately explains why they would come up in functional programming and immediately connects them right there to the category/type theoretic foundations whose myriad of incarnations we we are discussing in a multitude of guises here on the nnLab. For instance, following Spivak I would be able to immediately recognize lenses in, say proper equivariant \infty-bundle theory, and could maybe fruitfully interact with the lens community.

    But if you are right in #33 then this ought not to happen, then lenses are but a random hack which I’d better ignore.

    • CommentRowNumber35.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    I think I’m not getting across what I’m trying to convey, never mind me.

    • CommentRowNumber36.
    • CommentAuthorBryceClarke
    • CommentTimeJul 6th 2021

    Added a Properties section with three basic results in the literature: that lenses are algebras for a monad, that lenses in SetSet are equivalent to product projections, and that lenses in a Cartesian closed category are equivalent to coalgebras for a comonad.

    Also tidied up the Definition section with definition and remark environments (there was previously an issue with the labeling) and also reorganized the references into two broad classes: papers and other material. The should be sorted in chronological order, but if the list keeps growing it may be better to sort by kind of lenses they discuss. I added in some missing doi links as well.

    diff, v20, current

    • CommentRowNumber37.
    • CommentAuthorBryceClarke
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    EDIT: duplicate comment

    • CommentRowNumber38.
    • CommentAuthorBryceClarke
    • CommentTimeJul 6th 2021
    • (edited Jul 6th 2021)

    EDIT: duplicate comment

    • CommentRowNumber39.
    • CommentAuthorDavidRoberts
    • CommentTimeJul 6th 2021

    @Bryce

    if you do one edit with a comment, then go and do some tweaking, you can leave the comment section blank, and make some edits to the auto-generated comment here to reflect any additional information you feel needs to be included.

    • CommentRowNumber40.
    • CommentAuthorBryceClarke
    • CommentTimeJul 7th 2021

    Thanks. I think the issue was the original edit didn’t compile, and it took a couple of edits to fix, but I wasn’t aware this was also sending duplicate comments to the forum. I will be aware of this for the future!

    • CommentRowNumber41.
    • CommentAuthormattecapu
    • CommentTimeJul 7th 2021

    @Bryce is Proposition 3.1 replacing the comment after Definition 2.1 regarding lenses as algebras of the ’possibility monad’? If yes I’ll delete it in favor of the more organized version.

    • CommentRowNumber42.
    • CommentAuthormattecapu
    • CommentTimeJul 7th 2021

    Addressing #28

    diff, v21, current

    • CommentRowNumber43.
    • CommentAuthorBryceClarke
    • CommentTimeJul 11th 2021
    • (edited Jul 11th 2021)

    Shifted the remarks which previously followed the definition in reply to #41. Made a separate section title for the category whose morphisms are lenses. Split the Generalizations section into two subsections for lenses with laws and lenses without laws; there still needs to be more examples placed here from the literature.

    diff, v22, current

    • CommentRowNumber44.
    • CommentAuthorDavidJaz
    • CommentTimeSep 5th 2021

    Hi Everyone,

    I hope I’m not stepping on anybody’s toes with this edit, but I quite drastically re-wrote the introduction. I tried to remove the attitude (that there is something wrong or useless about the notion of lens), and to make clear right away that the name is used for two very different threads of thought — the lawful and lawless (aka polymorphic) lenses.

    I didn’t add any math, though I would like to come back and explain how David Spivak’s generalized lenses work because I think they are very nice. Hopefully someone with a more enclycopaedic knowledge of the topic can come and organize all the various definitions which have been floating around — there are a lot.

    I also separated the references to my and David’s (and Nelson Niu’s) books (since they are now separate books) which use (lawless, generalized) lenses for categorical systems theory.

    Cheers, David

    diff, v23, current

    • CommentRowNumber45.
    • CommentAuthorDavid_Corfield
    • CommentTimeSep 5th 2021
    • (edited Sep 5th 2021)

    Thanks for this, David. (Lots of Davids around here.)

    I wonder, is there any way to make the following less vague?:

    situations where some structure is converted to a different form – a view – in such a way that changes made to the view can be reflected as updates to the original structure.

    It seems to cover so much – representing a battlefield on a map, representing temperature by the height of a column,… Is there a distinctively lens-like situation?

  2. Added reference

    Bartosz Milewski

    diff, v24, current

    • CommentRowNumber47.
    • CommentAuthorRodMcGuire
    • CommentTimeSep 5th 2021
Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)