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). See http://www.cs.columbia.edu/~espinosa/ for 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. David -------------------- 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?