Inserting effects underneath others

[michaelpj]

I find myself wanting to have values with a very specific list of effects, to constrain what my users can do, e.g. Eff '[E1, E2] a.

However, I then have issues interpreting those: if E1 can be interpreted in terms of E3, I need to get E3 under E1 (and perhaps E2) in the stack.

But this seems hard to do. I've managed to write:
raiseBehind :: forall effs a . Eff '[a] ~> Eff (a ': effs)
but I can't figure out how to write
raiseBehindMany :: forall effs effs' . Eff effs ~> Eff (effs :++: effs')
although it seems like it should be sensical.

For the time being, I'm working around this by using
data SomeEffs effs a = SomeEffs { runSomeEffs :: forall effs' . Members effs effs' => Eff effs' a }
but this isn't very nice.

[lexi-lambda]

Can you ask your users to give you a value of type forall effs. Members '[E1, E2] effs => Eff effs a instead of Eff '[E1, E2] a?

[michaelpj]

Yes, but I find that type inference is awkward, whereas the SomeEffs version is nicer in that respect, but involves lots of wrapping and unwrapping. (This is kind of a general problem with existentials, I guess.)

I managed to hack together raiseBehindN for fixed N, copying polysemy, but it I can't figure out a version with an arbitrary list of effects on the front. Not the end of the world, but it feels like there isn't quite a single satisfactory solution.

[lexi-lambda]

Yes, but I find that type inference is awkward, whereas the SomeEffs version is nicer in that respect, but involves lots of wrapping and unwrapping. (This is kind of a general problem with existentials, I guess.)

Yes, I agree this is much less ergonomic than is ideal. I wish there were a better answer.

I have been (slowly) working in my spare time on effect systems. One of the recurring themes I have discovered in my exploration is the relationship between subtyping and polymorphism in effect systems, especially in the context of Haskell. Fundamentally, I find we are usually trying to model subtyping—we want Eff '[E1, E2] a to be a subtype of Eff '[E1, E2, E3] a, or even of Eff '[E2, E1] a. Of course, Haskell does not have subtyping, so we must use polymorphism instead: we quantify over the list of effects and express constraints on that list, but ultimately we eventually instantiate it to a single concrete list of effects.

At first blush these approaches seem equivalent, but even if we look past the ergonomic differences, the polymorphism approach has serious problems, especially for performance. Consider that if we have a function with the type

foo :: A -> Eff effs B

then we would hope that GHC would be able to optimize the body of foo based on the fact that it cannot possibly perform any effects—it must be a pure function. Sadly however, it cannot, as the implementation of >>= for Eff (regardless of implementation) eventually depends on the particular choice of effs. Another way to think about this is to ignore freer monads for a moment and to consider a function with a type like this:

foo :: Monad m => A -> m B

We would very much like GHC to be able to optimize such a function to a use of pure e for some expression e, but in fact it cannot—uses of >>= inside of foo will remain there because GHC knows nothing about laws. Code that might be optimized into a tight loop if the function were truly pure is instead forced to do lots of inefficient calls to an unknown function passed via the Monad dictionary.

---

The above is all something of a tangent, not related to your question directly. In the case of freer-simple, a function like raiseBehind is probably not any meaningfully less efficient than just using the constraint, since freer-simple doesn’t play nice with the optimizer anyway. But there’s something unsatisfying about it.

As for the question of implementing a generic raiseBehind function, it actually can be done, but you’d need to use typeclasses, since you need to influence runtime behavior based on compile-time information. You could write a class like

class RaiseBehind effs1 eff effs2 where
  raiseBehind :: Effs (effs1 :++: effs2) a -> Effs (effs1 :++: (eff ': effs2)) a

with instances of the following shape:

instance RaiseBehind '[] eff effs
instance RaiseBehind effs1 eff effs2 => RaiseBehind (eff1 ': effs1) eff effs2

However, type inference for such a method would be truly abysmal, as all three class parameters are ambiguous in the type of raiseBehind, so you’d have to pick them all explicitly with TypeApplications. Theoretically, GHC could do some inference if :++: had the right injectivity rules, but you’d need something like

type family as :++: bs = r | as r -> bs, bs r -> as

which is not supported today by TypeFamilyDependencies.

[michaelpj]

Fundamentally, I find we are usually trying to model subtyping—we want Eff '[E1, E2] a to be a subtype of Eff '[E1, E2, E3] a, or even of Eff '[E2, E1] a.

Yes, I agree. It seems like we want sets of effects with inclusion, and have the ordering of the handlers determine the nesting of the effects.

As for the question of implementing a generic raiseBehind function, it actually can be done, but you’d need to use typeclasses, since you need to influence runtime behavior based on compile-time information.

Yes, I tried to do something like this, but it's difficult to recurse "from the back" of a type level list specified with :++:. I had issues with GHC not being able to prove that effs :++: [] was equal to effs.

---

At any rate, it sounds like there's not much more to do here. Perhaps worth bearing in mind as a use-case for your future systems, though!