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

Есть ли какое-нибудь стандартное имя для конструктора типа 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

операция, которая заставляет это казаться некой «категорией в категории эндофункторов», но я не уверен, как это можно формализовать.

РЕДАКТИРОВАТЬ: Как указывает Чи, это связано с индексированной монадой: с учетом индексированной монады

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

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

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

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

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

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


haskell category-theory agda
person Anton Golov    schedule 21.02.2018    source источник
comment
Похоже на индексированную монаду, но не совсем то же самое (?)   -  person chi    schedule 21.02.2018
comment
Ах да, хороший момент, там есть связь.   -  person Anton Golov    schedule 21.02.2018
comment
Я бы все равно назвал это частным случаем (в стиле Atkey, а не в стиле Макбрайда) проиндексированной монады, она просто имеет некоторую дополнительную профункторность в индексах. Монада индексированного состояния, например, соответствует этому шаблону. (Роберт Этки представил их в статье, которую я связал, отсюда характерное название Макбрайда для типа клавиши at :=.)   -  person Benjamin Hodgson♦    schedule 21.02.2018
comment
@BenjaminHodgson Спасибо, это именно то, что я искал! Если вы опубликуете это как ответ, я приму это. (И Роберт Этки даже предвидел проблему, с которой, я думаю, я столкнусь с его требованиями к тензорному продукту.)   -  person Anton Golov    schedule 22.02.2018

Ответы (1)


arrow_upward
2
arrow_downward

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

Для категории 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 как объектами, обогащенными эндофункторами C. Hom-объект Hom(X, Y) это M X Y, а операции return и join, описанные в вопросе, снова дают начало требуемым семействам морфизмов.

person Anton Golov    schedule 05.03.2018