[Question] Why eliminating effects one-by-one?

[Heimdell]

Subj.

Doesn't it requre all eliminators (runX, runY, runZ) to be applied sequentally and independently to each argument of send? With your encoding, putting all eliminators in an array looks to me as more natural strategy. You loose efficient top-effect-removal, but running becomes as simple as (arr ! index) ... effect. At least, this array would be present in the cache all the time.

This can also spare you from having your output monad m being the last element of the effect stack - so you can now convert to any monad, not just the last one. Without some IO at the bottom you can declare that the code can't launch rockets, unless Launching effect is provided.

This is helpful - the user of the framework might want to not have IO monad necessarily stuck in her code, because some testing frameworks refuse to shrink or whatnot in IO cases.

Another advantage (or disadvantage)... Ok, lets call this a property: in array-of-dispatchers case, the order of effects is delayed until transformation into working monad, instead of being peeled in some predefined order. The order becomes fixed at the point you run the Effect effs () program.

Also, in what cases does the user want to eliminate effects one-by-one? This is not a question against that style of running, I'm just curious. Technically, you can do this in array case as well, by transforming to (pseudocode) Effects '(tail effs). I didn't try it, because I prefer the effect list to have "final" encoding, but it should be possible.

[isovector]

Thanks for raising the questions!

putting all eliminators in an array looks to me as more natural strategy

I'm not sure. I really like functions. I know how functions work and I know how they compose and how to abstract over them. I am way less certain about how to deal with arrays. Worse I have no idea what the semantics of such a thing are. If all my effects are evaluated simultaneously, how does a State effect interact with a caught Error? Does it have rollback semantics or not? With the one-by-one approach you get rollback semantics by ordering your functions one way, and a consistent view of the state the other.

Furthermore, if you eliminate effects one-by-one, it means you can eliminate them in places other than main. It means you can write in interpreters which themselves are defined in terms of other temporary effects. I don't know how I'd go about doing such a thing in a simultaneously interpreted environment.

This can also spare you from having your output monad m being the last element of the effect stack - so you can now convert to any monad, not just the last one.

I don't understand this. How can you convert to any monad? What is the meaning of converting to a monad that is not in your monad stack --- other than just calling pure? Monads are interesting because of their actions, and you can't call any of their actions if you don't know about them beforehand.

Without some IO at the bottom you can declare that the code can't launch rockets, unless Launching effect is provided.

I think this is adequately solved in the same way as mtl; you add a MonadIO m-equivalent constraint. But you do this only in your interpreters, not your application code. Now you can simply eliminate IO by just not calling any interpreters which do IO.

That being said, I like the idea of making it harder to use IO in application code. I am FIRMLY FIRMLY of the belief that raw IO has no place in business logic.

[Heimdell]

If all my effects are evaluated simultaneously, how does a State effect interact with a caught Error?

That depends entirely on the monad m you are converting to and the State s ~> m/Error e ~> m interpreters.

Furthermore, if you eliminate effects one-by-one, it means you can eliminate them in places other than main. It means you can write in interpreters which themselves are defined in terms of other temporary effects. I don't know how I'd go about doing such a thing in a simultaneously interpreted environment.

Actually, its still possible: You have an Effect (Eff1 ': effs) a and you interpret it into Effect effs a, thus removing the top effect.

I don't understand this. How can you convert to any monad?

newtype Effect (effs :: [Action]) (a :: Type) = Effect
    { runEffects :: ∀ m. Monad m => Dispatch effs m -> m a
    }

In my implementation, you provide a Dispatch effs m (which is an array of effN ~> m internally) for the monad m you want to convert to. Effect itself doesn't depend on the output monad.

What is the meaning of converting to a monad that is not in your monad stack?

It's not a stack, but rather a set of capabilities. You convert to a monad that supports those.

I think this is adequately solved in the same way as mtl.

That's fine, unless you have same problem mtl does - which is allowing only topmost layer of same transformer to be used.

That being said, I like the idea of making it harder to use IO in application code. I am FIRMLY FIRMLY of the belief that raw IO has no place in business logic.

I have the same goal.

There's an example code with simultaneous dispatch: https://bitbucket.org/heimdell/yo/src/master/src/Control/Effect/Example.hs

[Heimdell]

Actually, its still possible: You have an Effect (Eff1 ': effs) a and you interpret it into Effect effs a, thus removing the top effec

I tried it in my encoding and I failed, because peeler can't access inner action in Catch action handler. This can be solved by some template haskell code providing instances which help map the m in my effects (or some dishonest tricks).

So, I still have no proof that removal of top effect in my encoding is possible.

[Heimdell]

So, about making your implementation "freer" - what's the current problem?

[isovector]

Actually I think I've got it sorted out. The trick is getting the higher-order effects to preserve their state, even though you need to do a Coyoneda thing to delay all of the computations until the very end.

Currently blocked on getting the TH for smart constructors working, but this is more a problem of sitting down and doing it more than anything else.

[Heimdell]

https://bitbucket.org/heimdell/yo/src/master/src/Control/Effect/Example.hs?fileviewer=file-view-default#Example.hs-98

I've implemented effect removal; this operation is still not efficient, though. The remove operation has to recursively visit the whole tree.

[isovector]

@Heimdell have you benchmarked it? Try turning on -O2 -flate-specialise -fspecialise-aggressively and take a look at the core. You might get lucky and have GHC evaluate everything at compile time.

[Heimdell]

I expect specialiser to run away screaming after seeing that much unsafeCoerce in one module; but hey, the wonders can happen, I believe in it. Thank you for the flags, will definitely try.

[Heimdell]

I tried singleton-index-encoding and I can't construct any of reinterpret methods that allow doing interesting things. Its either ∀ m. Monad m => e m ~> Effect effs or ∀ m. Monad m => e m ~> m effect removal. Neither of them allows to re-handle subexpressions.

However, the basic functionality is working.

The interpret function of yours receives a ∀ x m. e m x -> Semantics r x function as argument. How is it possible to write non-trivial function of that type - that actually uses those m a inside a e m x value? Do you have any example usage of that?

[Heimdell]

FirstOrder e "interpret"

Oh, now I see.

[Heimdell]

I think, reinterpretH requires the user to have their end monad as a Lifted thing in their context.

[isovector]

I think, reinterpretH requires the user to have their end monad as a Lifted thing in their context.

I don't think so --- for example, look at runFixpoint

[Heimdell]

The Fixpoint looks like a special case. Basically, I think you have to push this monad to effect stack to dispatch it.

[isovector]

Sorry, I'm not sure I understand the claim --- reinterpretH doesn't require any Lifts

[Heimdell]

So, how do the Tactics work, in layman terms?

[isovector]

In "Effect Handlers in Scope", there is the notion of an Effect typeclass:

class Effect e where
  weave :: Functor s => s () -> (forall x. s (m x) -> n (s x)) -> e m a -> e n (s a)

which allows other effect handlers to push their state (some functor s) through e. weave is the crux of higher-order effects, since without it, you can't write any interesting interpretations.

Writing instances of Effect are actually quite annoying; you need to explicitly fmap const things inside of the s (), and then manually get everything to typecheck.

The Tactics effect is essentially a reader over the s () and forall x. s (m x) -> n (s x) bits of weave, and gives a lot of helpful combinators for actually implementing the function as part of a interpretH.