11

I've been reading a bit about the category theoric interpretation of Haskell Applicative functors: apparently, they can be interpreted in category theoretic terms as either lax closed functors or lax monoidal functors (depending on who you ask, it seems), and this made me wonder about the following.

A while ago, I wrote a paper (together with Ilya Sergey and our advisors Frank Piessens and Dave Clarke) about a recursion primitive for "effect recursion" in DSLs using Applicative functors, intended mainly for use in parser libraries. We found out that we needed a few quite special constructors that seem like they might be generalisable (somehow). In summary, what I'm asking is: are some of the below constructions somehow connected to category theory and if so, how?

Note that I will write p ◦ q for the composition of two applicative functors p and q.

Here is a list of the primitives we needed along the way:

  • afix: an effect recursion primitive. We really wanted a recursion primitive that looked like this:

    afix :: (p a → p a) → p a

    However, this was unimplementable for the more complex interpretations of p that we needed. Instead, we ended up with the following:

    afix :: (∀ q. Applicative q ⇒ p (q a) → p (q a)) → p a

    Apparently, wrapping values of the recursive occurrence in this parametrically quantified applicative functor q enforced a kind of value-effect separation in the function that we take the fixpoint of. Apparently, this was sufficient to make our more complex functions work.

  • Deeper in the implementation, we needed a sort of coapplicative operator that looks like this:

    coapp0 :: (p a → p b) → p (a → b)

    However, requiring this as a general operator for p, seems like it would have restricted us to only trivial applicative functors p. Instead, we noticed that we could make do with the following, which was implementable:

    coapp :: Applicative p ⇒ (∀ q . Applicative q ⇒ (p ◦ q) a → (p ◦ q) b) → p (a → b)

So in summary: is any of the above somehow familiar-looking from a category-theoretic point of view? Specifically, the restriction over functions of type ∀ q . Applicative q ⇒ (p ◦ q) a → (p ◦ q) b rather than p a -> p b seems like it might be fundamental somehow? Are there any links that might help us make more sense of this stuff than we were able to do in the past?

There are more details in the paper about the above and how we used it, in case anyone is interested.

Community
  • 1
  • 1
Dominique Devriese
  • 2,998
  • 1
  • 15
  • 21
  • 1
    This `coapp` smells of Kripke models. – pigworker Jan 26 '17 at 12:37
  • @pigworker: does that mean you see it as a kind of future-world quantification somehow? – Dominique Devriese Jan 26 '17 at 12:56
  • 1
    Yeah. In particular, taking q to be Maybe, you might be able to represent the formal parameter of the binding. – pigworker Jan 26 '17 at 13:36
  • 1
    It's similar to the type of a [`Prism`](https://hackage.haskell.org/package/lens-4.15.1/docs/Control-Lens-Prism.html) from the lens library, but without universal quantification over the outer functor. `type Prism s t a b = forall p f. (Choice p, Applicative f) => p a (f b) -> p s (f t)`. There's not a related type hanging around in `lens` for just the `Applicative q => p (q a) -> p (q b)` part (a less general prism). If you had a general prism `f`, `Star` would transform any `Applicative p` into a compatible profunctor to be able to pass `f` to `coapp` or `afix`. – Cirdec Jan 26 '17 at 18:44
  • I don't know if any _interesting_ prisms exist to pass to `coapp` or `afix`. It's likely that they're all trivial. – Cirdec Jan 26 '17 at 18:57
  • @pigworker: representing the formal parameter somewhat corresponds to an intuition I had about how the `∀ q. Applicative q ⇒ p (q a) → p (q a)` type enforced a kind of effect-values separation. My intuition was that the dependency of the returned `p a` on the argument `p a` (call it x) should take the form of a tree whose leaves are either occurrences of x or constant ps (i.e. any `p t` that doesn't depend on x) and whose branch points are formed by applications of the applicative `<*>`. – Dominique Devriese Jan 28 '17 at 20:08

0 Answers0