4
$\begingroup$

I am wondering if there is a good way to complete the following analogy:

monad : Kleisli category :: applicative functor : ??

That is, a given monad T on a category C gives rise to its Kleisli category C_T, whose objects are those of C, but whose morphisms between A and B are the morphisms between A and T(B) in C (Wikipedia entry). What I'd like to know is if there is a kind of "equivalent" notion for applicatives.

At first blush, it seems that such a category would be constructed in the following way, given a category C and an applicative functor (F : C -> C, pure, (<*>)). The category C_F is the one whose objects are taken from C (as above), but whose morphisms between A and B are in one-to-one correspondence with the morphisms between 1 and F(B^A) in C - that is, "elements" of F(B^A). In addition, identities and composition are given by:

id_(C_F)_A = pure id_C_A

f o_(C_F) g = pure (o_C) <*> f <*> g

where id_X_A is the identity on A in category X, and (o_X) is composition between morphisms in X.

$\endgroup$

3 Answers 3

3
$\begingroup$

Yes, your definition does give a category. This is an instance of a somewhat general construction called change of base from enriched category theory. There is an nlab page on the construction but if you are a programmer you might prefer to read Bartosz's chapter on enriched categories first.

In fact your definition uses change of base twice. Let $C$ be a cartesian-closed category we think of as our programming language.

  1. First, an applicative functor is a lax monoidal functor from $F : C \to C$.
  2. Second, we can think of $C$ as enriched over itself, called $s(C)$.
  3. Then we can do a change of base to define a $C$-enriched category $F_*(s(C))$ whose objects are the objects of $C$ and whose hom objects are F(a -> b)
  4. We can define a lax monoidal functor $\Gamma : C \to \text{Set}$ by sending each a to the set of morphisms from 1 to a.
  5. Then your category is $\Gamma_*(F_*(s(C)))$.
$\endgroup$
1
$\begingroup$

Your description of that category is correct.

We can define a lawful category of this kind. Objects are all types A, B, ... and morphisms between A and B are values of type F(A -> B). The identity morphism on A is unit(identity) of type F(A -> A). The composition operation of type F(A -> B) -> F(B -> C) -> F(A -> C) is defined via ap. The identity and associativity laws hold for that composition operation, as long as the applicative functor F is lawful (i.e., the laws of ap and pure hold), although it takes a bit of effort to prove that.

$\endgroup$
0
$\begingroup$

Thanks, all. Sometime after asking this, I was pointed to this paper, which gives a Haskell encoding of the relevant "Cayley" category in Sec. 3.4, p. 83.

$\endgroup$
2
  • $\begingroup$ Could you develop a bit your description of the answer described in the link? $\endgroup$
    – J..y B..y
    Apr 26 at 11:22
  • $\begingroup$ Not entirely sure which part to develop or clarify, but I had in mind that the 'C' in my original post corresponds to the 't' quantified in the instance declaration in Sec. 3.4, while my applicative 'F' corresponds to the quantified 'f'. $\endgroup$
    – Julian G.
    Apr 30 at 23:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.