Jason (jcreed) wrote,
Jason
jcreed

Have been looking at the literature on Functional Reactive Programming and related things. I am learning that no matter how much I think I've properly digested the whole world of monads and arrows and applicative functors, there's always more to learn.

Generally speaking the programmers' approach to all of these concepts seems very weird to me compared to the logician/category-theorist take, but McBride and Paterson's "Applicative programming with effects" is a really awesome paper that synthesizes the two points of view pretty well for the case of applicative functors. The punchline is that what a Haskell hacker calls applicative functors are what a category theorist calls strong lax monoidal functors. Yes, both strong and lax! Terribly, from a terminological point of view, "lax" means that the functor is weaker than "weak", and "strong" isn't the opposite of "weak" (if anything, "strict" is --- but since "lax" exists as a concept, it's hard to say that "strict" is the opposite of "weak", just that it's, ahem, a stronger condition than "weak") and means that the functor has a "strength".

Ok, everybody sufficiently confused now? Good.

The important thing about these strong but sensitive applicative functors is that they represent a notion of effect that is compatible with product types in one direction, and this very compatibility is a notion of sequencing of effects. Suppose T is an applicative functor. If I have a piece of data of type TA, which is a computation returning type A, and a piece of data of type TB, a computation returning B, then I can make T(A × B) by running the first one and then the second. I can't expect to necessarily do the reverse --- I might reasonably encounter a computation T(A × B) that doesn't naturally decompose into TA and TB. This one-way ticket is the laxness. For a weak monoidal functor would commute up to isomorphism with products, and you'd have T(A × B) isomorphic (with suitable coherence diagrams) to TA × TB, but a lax monoidal functor only goes one way. It needs to be a strong lax monoidal functor for the same reason that the monads in functional programming are always strong monads, to be compatible with our expectations about variable contexts.

But wait, I hear you saying, weren't we told that monads were the ultimate story on a pure functional treatment of effects and sequencing and stuff? Answer: they're one story, yes. The intuitive distinction between monads and applicatives (which the paper above explains rather nicely) is that monads, unlike applicatives, let you use the result of one computation to influence which other computation takes place as the second step. Just look at the Kleisli star's type, it's right there:

TA → (A → TB) → TB

The second argument gets the value of type A before it spits out the final computation. If T were just an applicative functor, the most we could make out of TA and (A → TB) would be TTB. When T is a monad, we have exactly the categorical μ to turn that into TB (this is of course exactly how the Kleisli star is implemented from the categorical data T, η, μ) but when T is merely applicative, TTB is considered a more complicated thingy than TB --- it has two stages of computational dependency, which we're not allowed to erase.
Tags: applicative functors, functional programming, monads
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 1 comment