类型构造函数的名称,它既是类别又是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. 我已经完成了在Agda的建设检查. 不过,我仍然想知道这个更有限的结构是否已知.

Answer 1

正如评论中指出的，这是 Robert Atkey 在他的参数化计算概念论文中引入的参数化 Monad 的概念。这对应于范畴论中对内函子范畴进行丰富的范畴的概念。

对于一个范畴来说C，要丰富于具有幺半群结构的范畴V(I, x)，意味着对于 的每个对象X，Y的CHom 对象Hom(X, Y)是 的对象V，并且存在给出恒等性和复合的态射 ，I -> Hom(X, X)和Hom(Y, Z) x Hom(X, Y) -> Hom(X, Z)。某些同一性和关联性条件必须成立，对应于范畴的同一性和关联性的通常要求。

M上的monadC可以被视为比 上的内函子丰富的单一对象类别C。由于只有一个对象X，因此也存在一个 Hom 对象Hom(X, X)，即M。返回操作产生恒等态射（自然变换）I -> M，连接操作产生复合态射（自然变换）M x M -> M。那么身份和关联性条件就与单子的条件完全对应。

参数化的单子MonC的参数取自某个集合，S可以被视为一个类别，其元素为S对象，丰富了 的内函子C。Hom 对象Hom(X, Y)是M X Y，问题中描述的return和join运算再次产生所需的态射族。