The idea of EffT es m

[ymdryo]

Hello. I’ve been very excited by the design of bluefin, especially its type-level machinery. In particular, I find it fascinating how it ensures scope safety by treating the set of type-level effects as the “s” in the usual ST (i.e. a collection of skolem type variables).

What I’d like to ask your opinion about is adding a generalization of the current Eff monad, which I’m calling EffT. The idea is to generalize the definition of Eff, which is currently fixed as IO a, to something like:

newtype EffT (es :: Effects) m a = UnsafeMkEffT (m a)
type Eff (es :: Effects) = EffT es IO

runEffT_
  :: (forall e. Emb m e -> EffT e m a)
  -> m a

(Or perhaps the order of the type parameters es and m would be better swapped.)

Here, Emb m is a generalization of IOE.

This would allow the bluefin effect system to be “stacked on top of” existing mtl-style monad ecosystems, improving interoperability. For example, if you want to use MegaParsec and you have a parser monad Parser a, you could write EffT es Parser and thus extend MegaParsec with bluefin effects. Additionally, this is also intended as a foundation for enabling future interoperability between heftia and bluefin.

However, I have two concerns:

• Added complexity in interface types.
  All of bluefin's interfaces would gain an extra m parameter, slightly undermining its current simplicity. I personally feel it would be quite a shame to confine the powerful type-level ideas in bluefin to IO only without generalizing them. I intuitively feel that the generalized form is the more natural one.

• Potential performance degradation.
  This might be mitigated by adding INLINE pragmas to various functions and, if needed, providing separate interfaces specialized for m = IO. Still, I’m not entirely confident we can make the performance fully match the pre-generalized version. If performance truly becomes an issue, there is always the option (though it would make maintenance a bit more cumbersome) of starting a completely separate module for EffT, independent of the existing bluefin codebase. So, I think we’ll probably be okay.

Perhaps this idea has already been considered and dismissed for such reasons. I’d love to hear your thoughts.
I'd also be happy to help with the implementation, if that's of interest.

[tomjaguarpaw]

You can have a look here for an attempt at something like that: https://github.com/tomjaguarpaw/ad/blob/master/Eff-Args/app/RoseMTL.hs#L85. Unfortunately I think it's not going to work.

• Firstly, there is a GHC issue preventing optimization: https://gitlab.haskell.org/ghc/ghc/-/issues/24371
• Secondly, Bluefin-style constraints are vulnerable to this issue arising from incoherent instances: https://discourse.haskell.org/t/bluefin-a-new-effect-system/9395/9

[ymdryo]

I see, thank you. It doesn't seem like it's going to be straightforward.