CODEWITHSUNDEEP
haskellagdacategory-theory
Komi Golov
Komi Golov

Reputation: 3471

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

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.

Upvotes: 12

Views: 205

Answers (1)

Komi Golov
Komi Golov

Reputation: 3471

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.

Upvotes: 2

Related Questions