I've been reading the functional pearl "Applicative programming with effects" by Conor McBride. His papers are always interesting, and this one is no exception. I really like how functional programmers bring in these mathematical concepts to ground their abstractions and give them a clear definition. In this case we get applicative style programming based in "applicative" functors (which as the paper describes are actually strong lax monoidal functors). I have a basic understanding of what it means to be a strong lax monoidal functor, but I would like to look more into it.
The reason that these functors are especially interesting to me is something McBride mentions along with the instance of applicative for functions. On an unrelated note, the fact that -> (as in a function a->b) is a type constructor is amazing to me. When giving the definition for pure, he mentions that it is the K combinator, and when giving the definition for the operator, he mentions that it is the S combinator. It is known that the combinator I can be constructed out of S and K, meaning that there is some connection between applicative functors and computation (as SKI is a system of universal computation). I don't know enough about category theory to work out the connection, somehow there is a situation in which computation can be described by some functor and its composition. Maybe there is even some functor that corresponds to the untyped lambda calculus (and maybe others for other lambda calculi?). I know of work describing lambda calculus in category theory, but normally they describe a category, not a functor. I really don't know where this leads, but the paper has as a resource "Premonoidal categories and notions of computation" which hopefully investigates this more.
No comments:
Post a Comment