monadoptics

Description

Experiment with using profunctor optics (NB: not Profunctor optics!) to adjust the effect layers of monadic computations. Not a usable library, but the concepts might be interesting to folks working on effect systems and the like. I recommend looking through the README below (including the aside if interested in the guts), then looking through the code (which might be slightly out of sync with the README in naming conventions etc.).

Examples

Running an abstract stateful computation with global state

Suppose we have a stateful, IO-ful computation written using mtl style:

computation :: (MonadState String m, MonadIO m) => m ()
computation = do
  put "this stuff is left over!"
  liftIO $ print "foo"
  pure ()

Since we're already in (at least) IO, we may reason that it's just as well to use IO to model our state. To do this, we can use a getter that discharges the MonadState s m constraint and adds an additional MonadIO constraint:

inIORef :: MonadIO m => IORef s -> HGetter' (StateT s m) m

Now we can edit our original computation and run it in IO (being left with nothing more than a MonadIO m constraint):

checkIORef :: Show a => IORef a -> IO ()
checkIORef ior = readIORef ior >>= print

test :: IO ()
test = do
  x <- newIORef ""

  computation ^. inIORef x
  -- > "foo"

  checkIORef x
  -- > "this stuff is left over!"

PS: Having the original computation actually depend on MonadIO isn't necessary to make this work, it's just there as an (admittedly tenuous) motivating circumstance.

Editing parts of a computation

Let's say we're using the free monad of a functor to model computations on a stack:

data StackF k
  = Push Int k
  | Top (Int -> k)
  | Pop k
  | Add k
  deriving Functor

type Stack = Free StackF

-- ... @Free@ boilerplate

Here is a sample computation:

calc :: Stack Int
calc = do
  push 3
  push 4
  add
  x <- top
  return x

Let's write (far more explicitly than is actually necessary) an interpreter for this computation:

runStack :: (MonadState [Int] m, MonadFail m, MonadIO m) => Stack a -> m a
runStack = \case
  (Pure x) -> do
    liftIO $ putStrLn "Done!"
    pure x
  (Free f) ->
    case f of
      Push n k -> do
        liftIO $ putStrLn $ "Push " ++ show n
        modify ((:) n)
        runStack k
      Top ik -> do
        (t : _) <- get
        liftIO $ putStrLn $ "Top: " ++ show t
        runStack $ ik t
      Pop k -> do
        liftIO $ putStrLn "Pop"
        modify tail
        runStack k
      Add k -> do
        (x : y : r) <- get
        liftIO $ putStrLn $ "Add " ++ show x ++ " to " ++ show y
        put (x + y : r)
        runStack k

The interpreter interprets into some abstract monad that implements MonadState [Int] (for holding the actual stack), MonadFail (for rejecting invalid operations), and MonadIO (for logging messages).

We can start with an empty stack in an IORef, and use the inIORef optic to evaluate the computation on the stack:

test :: IO ()
test = do
  x <- newIORef []

  runStack calc ^. inIORef x
  -- > Push 3
  -- > Push 4
  -- > Add 4 to 3
  -- > Top: 7
  -- > Done!

  checkIORef x
  -- > [7]

Fairly standard stuff. Now suppose for some reason we want to edit parts of the computation. For example, let's say we want to double every number that the computation pushes onto the stack.

The approach for doing so is shown below, but explaining the concept of a "descent" requires a regrettably lengthy aside.

<details><summary>Aside</summary>

Traversable ~monad~ functor transformers

One way to think about a computation in the free monad is as a "list" of functor layers. The layers are built up by recursively composing a coproduct of functors (our StackF type) with itself, and at the "bottommost" layer lies the identity functor.

You can envision an analogy with a standard list where the elements are a sum type. The list is built up by recursively tupling together elements from the sum type, with a unit element terminating the list. Of course the analogy only works up to a point: precisely the point where composition of functors differs from tupling of elements.

Now, standard lists are traversable "with respect to tupling" (as are many other containers). This is witnessed by their instance of the Traversable typeclass:

class Functor t => Traversable t
  where
  traverse :: Applicative f => (a -> f b) -> (t a -> f (t b))

Wherefore the "with respect to tupling" qualifer? It is from the mention of the Applicative typeclass, shown below with the tupling revealed by uncurrying [1]:

class Functor f => Applicative f
  where
  pure :: a -> f a
  liftA2 :: ((a, b) -> c) -> ((f a, f b) -> f c)

So there is an analogy between lists (the free "monoid of tupling") and the free monad (the free "monoid of layering").

Since lists are traversable "with respect to tupling", might it be the case that the free monad is traversable "with respect to layering"?

To answer this question, we must cook up a class analogous to Traversable that represents traversability with respect to layering. In turn, this task demands that we find an appropriate substitute for the Applicative typeclass Traversable refers to. What Applicative is to tupling, the new class must be to layering.

Let's first remember that what we are layering is functors * -> *, whereas what we tuple is proper types *. Keeping this in mind, here is an appropriately "elevated" substitute for the Functor superclass of Applicative:

type f ~> g = forall x. f x -> g x -- [2]

-- [3]
class HFunctor f
  where
  hfmap :: (Functor a, Functor b) => (a ~> b) -> f a ~> f b

Here then is our Composeative class, which describes "~monad~ functor transformers" that are to functor composition what Applicative is to tupling:

type (:.:) = Compose

-- [4]
class HFunctor t => Composeative t
  where
  lift :: Functor f => f ~> t f
  collect :: (Functor f, Functor g, Functor h) => (f :.: g ~> h) -> (t f :.: t g ~> t h)

Ignoring the functor constraints, perhaps you can see the analogy to the types of pure and liftA2 in the explicitly tupled Applicative typeclass.

Now we can return to traversability in layers. Here is a Descendable typeclass that shows what it means for a functor transformer to be traversable in the layers it "contains":

class HFunctor t => Descendable t
  where
  descend :: (Composeative f, Functor a, Functor b) => (a ~> f b) -> (t a ~> f (t b))

Once again, you might notice here how this rhymes with the type of traverse.

So finally we ask ourselves: is Free :: (* -> *) -> * -> * Descendable in the functor layers it "contains"? And the answer is yes (look through the codebase for the implementation).

An example of a Composeative monad transformer we might consider is StateT s :: (* -> *) -> * -> *. Thus one useful specialization of descend might be:

descend :: (f ~> StateT s f) -> Free f ~> StateT s (Free f)

This allows us to splice access to state into each layer of our computation Free f a, and end up with a stateful computation of the form s -> Free f (a, s). The overall computation depends on an initial state, and terminates with a result and a final state, having evaluated all state transitions grafted onto the intermediate layers.

I suspect (but haven't had the time or motivation to extensively investigate) that a lot of the monad transformers we work with day to day are Composeative, or at the very least support an instance of a class similar to Composeative with heavier constraints than Functor.

Traversables and traversals, descendables and descents

In profunctor optics libraries we have a notion of "traversals" (which represent a generalization of traversable instances) [5]:

type Bazaar a b t = forall f. Applicative f => (a -> f b) -> f t

class Traversing p
  where
  wander :: (s -> Bazaar a b t) -> p a b -> p s t

type Traversal s t a b = forall p. Traversing p => p a b -> p s t

Note that Bazaar a b t is equivalent to the following FunList a b t type for this purpose [6]:

data FunList a b t = Done t 
                   | More a (FunList a b (b -> t))

Because of various issues with higher rank quantification and impredicativity that start cropping up when we try to take Bazaar "one level up", we're going to work with FunList instead.

One way to think about FunList/Bazaar is that the Traversable typeclass is equivalent to:

class Functor t => Traversable t
  where
  traverse :: Applicative f => t a -> (a -> f b) -> f (t b)
  -- which is the same as
  traverse :: t a -> Bazaar a b (t b)
  -- which is the same as
  traverse :: t a -> FunList a b (t b)

Ok, good, so we know what the profunctor constraint for traversals is (Traversing), and we know a slight simplification of it (swap Bazaar for FunList). Let's find the appropriate "tupling to layering substitute" for FunList first.

By a sequence of reasoning that I won't get into here [7], I believe that what FunList is to tupling, the following OnionList is to layering:

-- Singleton natural numbers
data SNat n
  where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

-- @Onion n x@ is to layering functors what @Vec n x@ is to tupling elements
data Onion n f a
  where
  Core :: a -> Onion Z f a
  Layer :: f (Onion n f a) -> Onion (S n) f a

data OnionList a b t x
  where
  OnionList :: Onion n a r -> (Onion n b r -> t x) -> OnionList a b t x

Great, so now we know how to swap out the Bazaar/FunList. Now to our equivalent of the Traversing profunctor class, which we imaginatively call Descending.

First we need a higher order profunctor typeclass:

class HProfunctor (p :: (* -> *) -> (* -> *) -> *)
  where
  hdimap :: (a' ~> a) -> (b ~> b') -> p a b -> p a' b'

Here is its subclass Descending, for which hopefully the