The subject of free monads is resurfacing of late, as it does from time to time. What prompted this write-up is that Sandy Maguire followed up his post with a discussion about an impredicative encoding (aka final encoding) of free monads:

newtype Freer f a = Freer (forall m. Monad m => (forall t. f t -> m t) -> m a)

That is: given a monad m, and an interpretation of my operations (f) in that monad, I can build an m a.

As it happens, capabilities-as-type-classes, as embodied by the capability library, are essentially the same thing. Let me explain.

As far as I know, the subject of impredicative encoding of free monads was first tackled, as many good things, by Russell O’Connor, who calls them van Laarhoven free monads. His blog post is a fairly mathy read. But the key bit is this:

-- (ops m) is required to be isomorphic to (Π n. i_n -> m j_n)
newtype VLMonad ops a = VLMonad { runVLMonad :: forall m. Monad m => ops m -> m a }

Where Π n. i_n -> m j_n is mathematician’s way of saying forall n. i n -> m (j n). Up to a very small difference (rename i to f and pick the identity for j), this is indeed the same type. O’Connor then proves that this type is isomorphic to the usual presentation of free monads.

data Free f a = Return a | Free (f (Free f a))

Less is more

The comment, in Russell O’Connor’s snippet, is crucial in the proof. Without it you can’t establish the isomorphism between VLMonad and the traditional Free monad.

That’s because not all effects can be represented in free monads. The prime example is exception handlers. You can make a function

handle :: Free MyEffect a -> Free MyEffect a -> Free MyEffect a

But it would have the property that (handle s f) >>= k = handle (s >>= k) (f >>= k). That is: exceptions raised after exiting the handler would still be caught by the handler. It is not a useless function, but it is not an exception handler. This phenomenon is a property of the free monad construction. In the impredicative encoding, it can be thought of as a consequence of the fact that in forall a. f a -> m a, f cannot refer to m.

So, while being isomorphic to Free is a nice theoretical property, Russell O’Connor’s phrasing presents us with an opportunity: if we simply drop the comment restricting the form of ops, we get a less constrained free monad type which supports more effects. Therefore, we won’t pay much attention to it at all in the rest of the post.

Towards capability

Functions in VLMonad will look, as functions in a monad do, like

somefunction :: A -> VLMonad Ops B

Where Ops represent the possible effects. For instance, if you need a state effect, you would define Ops as

data Ops m = Ops
  { put :: Int -> m ()
  , get :: m Int
  }

But, after all, VLMonad is simply a newtype: we could very well inline its definition.

somefunction :: A -> forall m. Monad m => Ops m -> m B

The ordering of types and argument is not too idiomatic, though. So let’s rearrange them a little:

somefunction :: Monad m => Ops m -> A -> m B

If this may look like a familiar style of structuring effect, it is. See for instance the style advertised by Éric Torreborre in a recent blog post. It’s not really so much an alternative to free monads as a different presentation of free monads (albeit slightly more liberal, if, as per previous section, we ignore the restriction from O’Connor’s comment).

Personally, I find it rather tiresome to explicitly carry around the capabilities (the Ops thing) at every function call. I’d rather keep my function arguments for the program logic, and leave all the plumbing to the monad. Therefore, I turn Ops into a type class, and move it “left of the fat arrow”: really in Haskell A -> B and A => B mean the same thing, they only differ in whose responsibility it is to pass the arguments around.

somefunction :: (Monad m, Ops m) => A -> m B

The definition of Ops for a state effect would, then, become

class Ops m where
  put :: Int -> m ()
  get :: m Int

This is precisely the style of programming supported by the capability library (see also our announcement blog post).

Closing thoughts

Free monads, capabilities-as-records and capabilities-as-type-classes, are, essentially, three different flavours of the same thing (with free monads technically being the more restrictive of the three, as it can’t have exception handling effects).

Choosing between the three is, ultimately, a matter of taste. I really like capabilities-as-type-classes because it pushes the boilerplate outside of the domain logic.

At the end of the day, what really matters is the core idea shared by these three approaches: capabilities should be expressed in terms of the domain logic, not in terms of implementation details.