类型构造函数的名称，它既是类别又是monad？

Question

是否有任何带有操作的类型构造函数F :: * -> * -> * -> *的标准名称

return :: x -> F a a x
bind :: F a b x -> (x -> F b c y) -> F a c y

这是第一个参数中的逆变函子和第二个和第三个中的协变函子？特别是，这是否与类别理论中的任何类型构造相对应？

这些行动产生了一个

join :: F a b (F b c x) -> F a c x

使这看起来像某种“endofunctors类别中的类别”的操作，但我不确定这是如何正式化的。

编辑：正如志所指出的，这与索引的monad有关：给定一个索引的monad

F' : (* -> *) -> (* -> *)

我们可以使用Atkey构造

data (:=) :: * -> * -> * -> *
    V :: x -> (x := a) a

然后定义

F a b x = F' (x := b) a

得到我们想要的那种monad。 I've done the construction in Agda to check.我仍然想知道这个更有限的结构是否已知。

Answer 1

正如评论中指出的那样，这是Robert Atkey在他的Parametrised Notions of Computation论文中引入的参数化Monad的概念。这对应于在类别理论中丰富于一类内导体的类别的概念。

对于一个类别C是enriched over a category V with monoidal structure (I, x)意味着对于X的每个物体Y，C，Hom-object Hom(X, Y)是V的对象，并且存在赋予身份和组成的态射，I -> Hom(X, X)和Hom(Y, Z) x Hom(X, Y) -> Hom(X, Z)。某些同一性和相关性条件必须符合一类的同一性和相关性的通常要求。

在M上的monad C可以看作是C上的endofunctors丰富的单一对象类别。由于只有一个物体X，还有一个Hom-object Hom(X, X)，它是M。返回操作产生一个同一性态射，一个自然变换I -> M，并且连接操作产生一个组合态射，一个自然变换M x M -> M。然后，身份和相关性条件完全对应于monad的那些。

M上的参数化monad C参数取自某些集合S，可以看作是S元素作为对象的类别，丰富了C的endofunctors。 Hom-object Hom(X, Y)是M X Y，问题中描述的return和join操作再次产生了所需的态射系列。