Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.
When you're interpreting a higher-order effect and therefore working with Tactics, why do you usually need to recursively call the interpreter you are implementing right now? (other than "so that it typechecks")
Is it something like "call with current continuation" where you "resume" your interpreter after you're done with whatever Tactics stuff you were doing?
(guessing this also applies to Strategy)
So that the effect gets interpreted in actions passed as arguments too?
The recursive call is actually a feature: we could implement interpretH so that it would do that for you. The reason we don't is because maybe you don't want to recurse with the exact same interpreter! runWriter and runReader are examples of this.
runReader is good example in particular: upon a Local f m, we recurse with runT m >>= \m' -> raise (runReader (f i) m'), where i is the input argument given to runReader.
Local f m
runT m >>= \m' -> raise (runReader (f i) m')