Is it possible to form the Kleisli category of several monads at once? I can imagine an indexed product of the individual Kleisli categories, but I lack the technical facility to describe it.
In my thesis, I have a category with multiple monads, relating the different "levels" of a denotational semantics (environments, stores, etc. More info
The monad laws follow easily from the Kleisli formulation; they say that the Kleisli category is actually a category. The monad morphism laws say that an arrow between monads is a functor between Kleisli categories. What I expect from a "multi-Kleisli" formulation is that Kleisli compositions associate (when possible).
Specifically, given monads P and PQ (where Q is another functor) and arrows f: A -> PQB, g: QB -> PQC, h: C -> PQD, we'd like
(oPQ (oP f g) h) = (oP f (oPQ g h))where oP and oPQ are the Kleisli compositions of the monads.
I can postulate a category with this structure, but it would be nicer if it came from a general construction.
P.S. Other formulations of associativity are:
;; bindT: TA * (A -> TB) -> TB
f: A -> PQB, g: QB -> PQC
(bindP (bindPQ pqa f) g) = (bindPQ pqa (lambda (a) (bindP (f a) g)))
;; mapT: (A -> B) * TA -> TB
;; joinT: TTA -> TA
;; f: A -> PQB, ;; g: QB -> PQC
(joinP (mapP g (joinPQ (mapPQ f pqa))))
= (joinPQ (mapPQ (lambda (a) (joinP (mapP g (f a)))) pqa))
Can we rewrite this using join in a more natural way?