Name for a type constructor that is both a category and a monad?

Question

Is there any standard name for a type constructor F :: * -> * -> * -> * with operations

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

that is a contravariant functor in the first argument and a covariant functor in the second and third? In particular, does this correspond to any kind construction in category theory?

The operations give rise to a

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

operation that makes this seem like some kind of "category in the category of endofunctors", but I'm not sure how that could be formalised.

EDIT: As chi points out, this is related to the indexed monad: given an indexed monad

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

we can use the Atkey construction

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

and then define

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

to get the kind of monad we want. I've done the construction in Agda to check. I'd still like to know whether this more limited structure is known, though.

It looks similar to an indexed monad, but not quite the same (?) — chi
I'd still call it a special case of an (Atkey-style, not McBride-style) indexed monad, it just has some additional profunctor-ness in the indices. The indexed state monad, for example, fits this pattern. (Robert Atkey introduced these in the paper I linked, hence McBride's characteristically punning name for the "at key" type :=.) — Benjamin Hodgson
@BenjaminHodgson Thanks, this is exactly what I was looking for! If you post it as an answer I'll accept it. (And Robert Atkey even anticipated a problem I think I'll run into with his tensor product requirement.) — Anton Golov

Anton Golov Anton Golov · Accepted Answer · 2018-03-05T08:57:04

As pointed out in the comments, this is the notion of a Parametrised Monad introduced by Robert Atkey in his Parametrised Notions of Computation paper. This corresponds to the notion of a category enriched over a category of endofunctors in category theory.

For a category C to be enriched over a category V with monoidal structure (I, x) means that for every objects X, Y of C, the Hom-object Hom(X, Y) is an object of V, and there exist morphisms that give the identity and composition, I -> Hom(X, X) and Hom(Y, Z) x Hom(X, Y) -> Hom(X, Z). Certain idenity and associativity conditions must hold, corresponding to the usual requirements of identity and associativity for a category.

A monad M on C can be seen as a one-object category enriched over endofunctors on C. Since there is only one object X, there is also one Hom-object Hom(X, X), which is M. The return operation gives rise to an identity morphism, a natural transformation I -> M, and the join operation gives rise to a composition morphism, a natural transformation M x M -> M. The identity and associativity conditions then correspond exactly to those of a monad.

A parametrised monad M on C with parameters taken from some set S can be seen as a category with elements of S as objects, enriched over the endofunctors of C. The Hom-object Hom(X, Y) is M X Y and the return and join operations described in the question again give rise to the families of morphisms required.

Name for a type constructor that is both a category and a monad?

1 Answers