强Dinatural变换与广义Codensity单子

我们引入dicodensity单子：对点态codensity单子的一个推广，其由混合变体双函数组成的单子。我们的构造基于强dinatural性（也称为巴里dinatural性）的概念，灵感来自于多态λ演算中某些类型的阴释模型——特别是带有普遍量化变量的Continuation单子的一种形式，例如System F中list单子的教堂编码。扩展一些关于Cayley式表示的先前结果，我们提供了一组充分条件，用于建立单子与其给定双函数组成的dicodensity单子之间的同构。然后，我们关注由我们的构造在hom函子上实例化并更一般地由由内部化hom集（即Eilenberg--Moore代数之间的内化hom集合）给出的双函数组成的单子。这给我们提供了，例如，对用于建模有序非确定性计算的各种semiring及其他理论的单子的一个新表述。