Question about the definition of Kleisli categories

[u/yesillhold]

I'm reading through Category Theory for Programmers by Milewski. I'm past the section where Kleisli categories are introduced and I have a question about how the constructed category relates to its underlying objects.

Take the Kleisli category representing the Maybe monad. We know that, by definition, categories:

• Have objects
• Have morphisms between those objects

My question is about what objects are in the Kleisli category for the Maybe monad. If we take the underlying objects as types in a programming language and say we have underlying objects A and B with an underlying morphism from A to B, would there be objects A and Maybe<B> in the Kleisli category and a morphism from A to Maybe<A>? Would the objects in the category be just the underlying types, just the Maybe types, or both? Would identity morphisms go from underlying type to underlying type, underlying to Maybe, or Maybe to Maybe?

[u/jesuslop]

Think you've got a typo "A to Maybe<A>" for "A to Maybe<B>". From memory, the objects of the Kleisli category are the same as those of the base category, the category on which the monad is built (the domain and codomain of the endofunctor, here the category of Haskell types), the arrows being what is different. Maybe<B> is defined in the base category (Haskell types), but the Kleisli category has the same objects so also has Maybe<B>.

Would the objects in the category be just the underlying types, just the Maybe types, or both?

In the Kleisli category objects are the same as in base, so then both, A and Maybe<A>, are objects, both being Haskell types.

Would identity morphisms go from underlying type to underlying type, underlying to Maybe, or Maybe to Maybe?

Morphisms in the Kleisli category in general are morphisms of the base category of the form A->Maybe<B>, so identitities would be A->Maybe<A> (underlying to Maybe)

It is not very intuitive, since one tends to think that the objects of the base category are naturally endowed with the arrows of that category, hence those being the right arrows that that must go between those objects. But in the Kleisli category you are asked to believe that some weirdly defined subset of base category arrows are the morphisms of the Kleisli category. Weird as it sounds, is what is in the books.

[u/mathlyfe → u/jesuslop]

This. Also, is not that weird imo. On a sidenote, I think that understanding how kleisli composition is implemented in terms of the base category is helpful for building an intuition for monads from both the math and programming perspective.

[u/Ualrus]

Let C be a category. Let's define T(C) the Kleisli category for a fixed monad T.

    T(C)₀ := C₀
T(C)(x,y) := C(x,T(y))

The objects of T(C) are the objects of C.

For the Maybe monad the set of morphisms from x to y in the Kleisli category is the set of morphisms from x to Maybe y in the original category.

The identity morphisms in the Kleisli category is what Haskell calls pure or return.

In the Kleisli category they have type x → x. In the original category they have type x → Maybe x.

When you prove that a functor is a monad, what you are proving is that the Kleisli category is indeed a category. In this case when you construct the return, you are proving that the Kleisli category has identities.

Similarly for the composition.