{"ID":2858648,"CreatedAt":"2026-06-01T04:54:23.091178241Z","UpdatedAt":"2026-06-01T04:54:23.091178241Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2510.06777","arxiv_id":"2510.06777","title":"Strong Dinatural Transformations and Generalised Codensity Monads","abstract":"We introduce dicodensity monads: a generalisation of pointwise codensity monads generated by functors to monads generated by mixed-variant bifunctors. Our construction is based on the notion of strong dinaturality (also known as Barr dinaturality), and is inspired by denotational models of certain types in polymorphic lambda calculi - in particular, a form of continuation monads with universally quantified variables, such as the Church encoding of the list monad in System F. Extending some previous results on Cayley-style representations, we provide a set of sufficient conditions to establish an isomorphism between a monad and the dicodensity monad for a given bifunctor. Then, we focus on the class of monads obtained by instantiating our construction with hom-functors and, more generally, bifunctors given by objects of homomorphisms (that is, internalised hom-sets between Eilenberg--Moore algebras). This gives us, for example, novel presentations of monads generated by different kinds of semirings and other theories used to model ordered nondeterministic computations.","short_abstract":"We introduce dicodensity monads: a generalisation of pointwise codensity monads generated by functors to monads generated by mixed-variant bifunctors. Our construction is based on the notion of strong dinaturality (also known as Barr dinaturality), and is inspired by denotational models of certain types in polymorphic...","url_abs":"https://arxiv.org/abs/2510.06777","url_pdf":"https://arxiv.org/pdf/2510.06777v4","authors":"[\"Maciej Piróg\",\"Filip Sieczkowski\"]","published":"2025-10-08T09:00:13Z","proceeding":"cs.LO","tasks":"[\"cs.LO\",\"cs.PL\"]","methods":"[]","has_code":false}
