Recursive calls in Tactics - Polysemy

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

Georgi Lyubenov // googleson78

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?

Love Waern (King of the Homeless)

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.

Love Waern (King of the Homeless)

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.