OKay so this is both my thesis and research work so I think it should go here before it goes into my thesis: I’ve been exploring how to push effects outside of the container language for as much as possible. Previously I was using lenses enriched in a monad to model effects in the forward part.
TO be perfectly comprehensive, the problem i have is as follows:
I have a function that is paired with a function . Ideally I would like those two to form a lens But of course the monad gets in the way.
To address this, I have been using morphisms of the form This works, but it’s a little bit unsastifactory because it introduces effects inside the lenses, but we would like to have them be outside so we can have better control of them. We can reduce the proliferation of effects using the “functor application” operator which I define like so
and monad-enriched lenses compose with functor-applied lenses so composes with to form , that helps but it’s still not great.
That’s the old approach, now here is the new approach:
Instead of pairing up with , we are going to think of as the costate lens and as the continuation from . The only reasonable way of combining those two this way is with a lens of type and treat as the effect of the lens . This is of course a co-parameterised lens where the monoidal product used is composition . Another way to see this lens is as a writer monad that add an effect token, but doesn’t actually perform the effect, it only declares a pair of input-output that needs to be executed by an external handler.
We see this notion of handler when we try to turn those lenses into executable programs. A lens becomes executable when we give it a costate (or a handler) for b . Whenever we deal with a coparameterised lens, we need to give two handlers: one for the effects and one for the codomain that is, becomes executable if we have and .
Now where does that leave us wrt to effectful computation using a monad in ? well it turns out there is a more powerful version of the effect handler above. we can write the following: That is. Given a parameterised lens and two effectful handlers, we can compose the lense with its effectful handlers and obtain an effectful costate lens in this case isomorphic to a function . All this even if the original lens has ZERO effectful computation in Set. It also allows the user to chose at a later date, leaving the effect specification only for running the program later, not as part of its specification originally.
I’m still exploring how this is used when combined with kleisli category of monads on containers (typically Maybe : Cont -> Cont) and I’m not done with my basic prototype that uses m = IO and reads a file off the filesystem, but so far, things seem to be working as expected