Имя для конструктора типа, который является как категорией, так и монадой?

Существует ли стандартное имя для конструктора типов 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

что делает это похоже на какую-то "категорию в категории эндофенторов", но я не уверен, как это можно было бы формализовать.

EDIT: Как указывает ци, это связано с индексированной монадой: с учетом индексированной монады

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

мы можем использовать конструкцию Atkey

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

и затем определите

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

чтобы получить желаемую монаду. Я проделал строительство в Агда, чтобы проверить. Я все равно хотел бы знать, известна ли эта более ограниченная структура.

Ответ 1

Как отмечалось в комментариях, это понятие "параметризованной монады", введенное Робертом Аткимом в его статье " Параметризированные понятия вычисления". Это соответствует понятию категории, обогащенной категорией эндофенторов в теории категорий.

Для категории C обогащенной над категорией V с моноидальной структурой (I, x) означает, что для любых объектов X, Y из C Hom-объект Hom(X, Y) является объектом V и существуют морфизмы I → Hom(X, X) и Hom(Y, Z) x Hom(X, Y) → Hom(X, Z). Должны выполняться определенные условия существования и ассоциативности, соответствующие обычным требованиям идентичности и ассоциативности для категории.

Монада M на C можно рассматривать как категорию с одним объектом, обогащенную над эндофунториальными элементами на C Поскольку существует только один объект X, существует также один Hom-объект Hom(X, X), который является M Возвратная операция порождает тождественный морфизм, естественное преобразование I → M, а операция объединения порождает композиционный морфизм, естественное преобразование M x M → M Условия идентичности и ассоциативности тогда точно соответствуют условиям монады.

Параметризованная монада M на C с параметрами, взятыми из некоторого множества S можно рассматривать как категорию с элементами S как объекты, обогащенную над endofunctors of C Hom-объект Hom(X, Y) является MXY а операции return и join описанные в вопросе, снова порождают семейства требуемых морфизмов.