Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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.

like image 709
Anton Golov Avatar asked Feb 21 '18 08:02

Anton Golov


1 Answers

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.

like image 95
Anton Golov Avatar answered Jan 29 '23 08:01

Anton Golov