What you have here is the immediate consequence of this construction being a category.
- Yes, they do conform. And that they conform is indeed the reason they are called Kleisli, because the Kleisli arrows plus types form the Kleisli category of the monad (to which every monad gives rise to). It's also why
unit
is called like that: it is the unit under composition of Kleisli arrows. - Yes, they can be derived. Use the transformation
(f <=< g) x = f =<< (g x)
(where<=<
isandThen
, and=<<
is probably something likeflip(bind)
in Scala). The exact steps of the derivation can be found here.