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)
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.
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
andrunReader
are examples of this.runReader
is good example in particular: upon aLocal f m
, we recurse withrunT m >>= \m' -> raise (runReader (f i) m')
, wherei
is the input argument given torunReader
.