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.

翻译：我们引入双余密度单子：这是一种对点态余密度单子的推广，从由函子生成的单子扩展为由混合变差双函子生成的单子。我们的构造基于强双自然性（亦称Barr双自然性）的概念，并受到多态lambda演算中特定类型的指称语义模型的启发——尤其是具有全称量化变量的某种延续单子形式，例如System F中列表单子的Church编码。通过扩展先前关于Cayley风格表示的一些结果，我们提供了一组充分条件，用于建立给定双函子的双余密度单子与某单子之间的同构关系。随后，我们重点关注通过用hom-函子实例化该构造所获得的单子类，更一般地，由同态对象（即Eilenberg-Moore代数间的内化hom集）给出的双函子所生成的单子。这使我们能够获得新颖的单子表示，例如由不同类型的半环及其他用于建模有序非确定性计算的理论所生成的单子。