haskell - 既是类别又是单子(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

使这看起来像是某种“内仿函数类别中的类别”的操作，但我不确定如何将其形式化。

编辑:正如 chi 指出的，这与索引单子(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 对象 Hom(X, Y)是 V 的对象，并且存在给出同一性和组成的态射，I -> Hom(X, X)和 Hom(Y, Z) x Hom(X, Y) -> Hom(X, Z) .一定的同一性和关联性条件必须保持，对应于一个类别的同一性和关联性的通常要求。

一个单子(monad) M在 C可以看作是在 C 上丰富了内仿函数的单对象类别。 .由于只有一个对象X , 还有一个 Hom-object Hom(X, X) ，即 M .返回操作产生恒等态射，自然变换I -> M ，并且连接操作会产生一个组合态射，一个自然变换 M x M -> M .然后，身份和关联性条件与单子(monad)的条件完全对应。

参数化的 monad M在 C参数取自某个集合 S可以看作是一个类别，其元素为 S作为对象，丰富了 C 的内仿函数. Hom对象Hom(X, Y)是 M X Y和 return和 join问题中描述的操作再次产生所需的态射族。