arXiv Science⌕ Search

arXiv subjects

Mario Román

Publications and source records attributed to Mario Román.

29 records · Page 2Linked to original sources
arXiv2024

Profunctor Optics, a Categorical Update

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.

cs.PL↗
arXiv2023

Optics for Premonoidal Categories

We further the theory of optics or "circuits-with-holes" to encompass premonoidal categories: monoidal categories without the interchange law. Every premonoidal category gives rise to an effectful category (i.e. a generalised Freyd-category) given by the embedding of the monoidal subcategory of central morphisms. We introduce "pro-effectful" categories and show that optics for premonoidal categories exhibit this structure. Pro-effectful categories are the non-representable versions of effectful categories, akin to the generalisation of monoidal to promonoidal categories. We extend a classical result of Day to this setting, showing an equivalence between pro-effectful structures on a category and effectful structures on its free tight cocompletion. We also demonstrate that pro-effectful categories are equivalent to prostrong promonads.

math.CT↗
arXiv2023

Collages of String Diagrams

We introduce collages of string diagrams as a diagrammatic syntax for glueing multiple monoidal categories. Collages of string diagrams are interpreted as pointed bimodular profunctors. As the main examples of this technique, we introduce string diagrams for bimodular categories, string diagrams for functor boxes, and string diagrams for internal diagrams.

math.CT↗
arXiv2023

Cornering Optics

We show that the category of optics in a monoidal category arises naturally from the free cornering of that category. Further, we show that the free cornering of a monoidal category is a natural setting in which to work with comb diagrams over that category. The free cornering admits an intuitive graphical calculus, which in light of our work may be used to reason about optics and comb diagrams.

math.CT↗
arXiv2023

The Produoidal Algebra of Process Decomposition

We introduce the normal produoidal category of monoidal contexts over an arbitrary monoidal category. In the same sense that a monoidal morphism represents a process, a monoidal context represents an incomplete process: a piece of a decomposition, possibly containing missing parts. We characterize monoidal contexts in terms of universal properties. In particular, symmetric monoidal contexts coincide with monoidal lenses, endowing them with a novel universal property. We apply this algebraic structure to the analysis of multi-party interaction protocols in arbitrary theories of processes.

cs.LO↗
arXiv2022

Span(Graph): a Canonical Feedback Algebra of Open Transition Systems

We show that Span(Graph)*, an algebra for open transition systems introduced by Katis, Sabadini and Walters, satisfies a universal property. By itself, this is a justification of the canonicity of this model of concurrency. However, the universal property is itself of interest, being a formal demonstration of the relationship between feedback and state. Indeed, feedback categories, also originally proposed by Katis, Sabadini and Walters, are a weakening of traced monoidal categories, with various applications in computer science. A state bootstrapping technique, which has appeared in several different contexts, yields free such categories. We show that Span(Graph)* arises in this way, being the free feedback category over Span(Set). Given that the latter can be seen as an algebra of predicates, the algebra of open transition systems thus arises - roughly speaking - as the result of bootstrapping state to that algebra. Finally, we generalize feedback categories endowing state spaces with extra structure: this extends the framework from mere transition systems to automata with initial and final states.

math.CT↗
arXiv2022

Open Diagrams via Coend Calculus

Morphisms in a monoidal category are usually interpreted as processes, and graphically depicted as square boxes. In practice, we are faced with the problem of interpreting what non-square boxes ought to represent in terms of the monoidal category and, more importantly, how should they be composed. Examples of this situation include lenses or learners. We propose a description of these non-square boxes, which we call open diagrams, using the monoidal bicategory of profunctors. A graphical coend calculus can then be used to reason about open diagrams and their compositions.

math.CT↗
arXiv2022

Monoidal Streams for Dataflow Programming

We introduce monoidal streams: a generalization of causal stream functions to monoidal categories. In the same way that streams provide semantics to dataflow programming with pure functions, monoidal streams provide semantics to dataflow programming with theories of processes represented by a symmetric monoidal category. At the same time, monoidal streams form a feedback monoidal category, which can be used to interpret signal flow graphs. As an example, we study a stochastic dataflow language.

cs.LO↗
arXiv2020

Comb Diagrams for Discrete-Time Feedback

The data for many useful bidirectional constructions in applied category theory (optics, learners, games, quantum combs) can be expressed in terms of diagrams containing "holes" or "incomplete parts", sometimes known as comb diagrams. We give a possible formalization of what these circuits with incomplete parts represent in terms of symmetric monoidal categories, using the dinaturality equivalence relations arising from a coend. Our main idea is to extend this formal description to allow for infinite circuits with holes indexed by the natural numbers. We show how infinite combs over an arbitrary symmetric monoidal category form again a symmetric monoidal category where notions of delay and feedback can be considered. The constructions presented here are still preliminary work.

cs.LO↗
arXiv2020

Profunctor optics and traversals

Optics are bidirectional accessors of data structures; they provide a powerful abstraction of many common data transformations. This abstraction is compositional thanks to a representation in terms of profunctors endowed with an algebraic structure called Tambara module. There exists a general definition of optic in terms of coends that, after some elementary application of the Yoneda lemma, particularizes in each one of the basic optics. Traversals used to be the exception; we show an elementary derivation of traversals and discuss some other new derivations for optics. We relate our characterization of traversals to the previous ones showing that the coalgebras of a comonad that represents and split into shape and contents are traversable functors. The representation of optics in terms of profunctors has many different proofs in the literature; we discuss two ways of proving it, generalizing both to the case of mixed optics for an arbitrary action. Categories of optics can be seen as Eilenberg-Moore categories for a monad described by Pastro and Street. This gives us two different approaches to composition between profunctor optics of different families: using distributive laws between the monads defining them, and using coproducts of monads. The second one is the one implicitly used in Haskell programming; but we show that a refinement of the notion of optic is required in order to model it faithfully. We provide experimental implementations of a library of optics in Haskell and partial Agda formalizations of the profunctor representation theorem.

cs.PL↗