On a fibrational construction for optics, lenses, and Dialectica categories

Reference. On a fibrational construction for optics, lenses, and Dialectica categories

Categories of lenses/optics and Dialectica categories are both comprised of bidirectional morphisms of basically the same form. In this work we show how they can be considered a special case of an overarching fibrational construction, generalizing Hofstra’s construction of Dialectica fibrations and Spivak’s construction of generalized lenses. This construction turns a tower of Grothendieck fibrations into another tower of fibrations by iteratively twisting each of the components, using the opposite fibration construction.

Cite

Cite as @capucci-2024-onx (helia, typst) · \cite{capucci-2024-onx} (LaTeX)

BibTeX

bibtex · 1 line

@article{capucci-2024-onx, title={On a fibrational construction for optics, lenses, and Dialectica categories}, volume={4}, ISSN={2969-2431}, url={http://dx.doi.org/10.46298/entics.14638}, DOI={10.46298/entics.14638}, journal={Electronic Notes in Theoretical Informatics and Computer Science}, publisher={Centre pour la Communication Scientifique Directe (CCSD)}, author={Capucci, Matteo and Gavranović, Bruno and Malik, Abdullah and Rios, Francisco and Weinberger, Jonathan}, year={2024}, month=Dec }

hayagriva YAML (typst)

yaml · 19 lines

capucci-2024-onx:
  type: article
  title: On a fibrational construction for optics, lenses, and Dialectica categories
  author:
  - Capucci, Matteo
  - Gavranović, Bruno
  - Malik, Abdullah
  - Rios, Francisco
  - Weinberger, Jonathan
  date: 2024-12
  url: http://dx.doi.org/10.46298/entics.14638
  serial-number:
    doi: 10.46298/entics.14638
    issn: 2969-2431
  parent:
    type: periodical
    title: Electronic Notes in Theoretical Informatics and Computer Science
    publisher: Centre pour la Communication Scientifique Directe (CCSD)
    volume: 4

Download: capucci-2024-onx.bib · capucci-2024-onx.yml

Cites 22 works (4 here)

With notes (4)

Profunctor Optics, a Categorical Update clarke-2024-profunctorCompositionality · 2024

Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. However, functional programming languages are arguably better described by enriched categories; and we have found that some structures in the literature are actually mixed optics, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.

DOI · arXiv

Towards Foundations of Categorical Cybernetics capucci-2022-towardsEPTCS · 2022

DOI · arXiv

Fibre optics braithwaite-2021-fibrearXiv · 2021

Lenses, optics and dependent lenses (or equivalently morphisms of containers, or equivalently natural transformations of polynomial functors) are all widely used in applied category theory as models of bidirectional processes. From the definition of lenses over a finite product category, optics weaken the required structure to actions of monoidal categories, and dependent lenses make use of the additional property of finite completeness (or, in case of polynomials, even local cartesian closure). This has caused a split in the applied category theory literature between those using optics and those using dependent lenses. The goal of this paper is to unify optics with dependent lenses, by finding a definition of fibre optics admitting both as special cases.

arXiv

Profunctor Optics: Modular Data Accessors pickering-2017-profunctorProgramming · 2017

DOI

External (18)

Dependent Optics (2023)
Actegories for the Working Mathematician (2023)
Polynomial functors: A mathematical theory of interaction (2023)
Seeing double through dependent optics (2022)
Compound Optics (2022)
Dependent products of polynomials (talk) (2022)
Categorical Systems Theory (book draft) (2022)
Cartesian Factorization Systems and Grothendieck Fibrations (2021)
Generalized lens categories via functors C^op -> Cat (2019)
Lenses for philosophers (2018)
The Dialectica monad and its cousins (2011)
Comment on 'the n-Category Cafe' (ternary factorization systems) (2010)
Combinators for bidirectional tree transformations (2007)
Distributors at Work (2000)
Some properties of Fib as a fibred 2-category (1999)
Comprehension categories and the semantics of type dependency (1993)
The Dialectica categories (1989)
Locally cartesian closed categories and type theory (1984)