Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: mutual recursion


view this post on Zulip Reid Barton (Oct 18 2020 at 15:14):

meta functions still can't be mutually recursive unless they're defined in a common mutual def, right? Any neat tricks to get around this if the definitions might be very long?

view this post on Zulip Reid Barton (Oct 18 2020 at 15:16):

One thing I was considering is basically an explicit translation to using fix, with a structure that holds the mutually recursive functions passed as an argument to each function

view this post on Zulip Reid Barton (Oct 18 2020 at 15:16):

and then tying the knot at the end

view this post on Zulip Reid Barton (Oct 18 2020 at 15:24):

This would be in the tactic monad. So another option could be to put the functions to be called recursively in a monad transformer or in global state or something like that. But none of these options sound especially appealing...

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:03):

If you can limit the number of functions that need to be called, you can pass them as an argument to all the helper functions, and then eventually you get to the main function and use an unguarded recursion there

view this post on Zulip Reid Barton (Oct 18 2020 at 16:04):

By "limit the number" you mean, say, I have just three functions such that if I remove calls into these functions, the call graph becomes acyclic?

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:04):

yes

view this post on Zulip Reid Barton (Oct 18 2020 at 16:05):

Right, that's basically what I'm considering with the structure of functions then

view this post on Zulip Reid Barton (Oct 18 2020 at 16:05):

I just have a gut feeling that, say, a 500-line mutual def is a bad idea, even if I don't know exactly why...

view this post on Zulip Mario Carneiro (Oct 18 2020 at 16:07):

I have the same feeling. It compiles slower and you can't put docs on it properly

view this post on Zulip Reid Barton (Oct 18 2020 at 17:25):

A hidden bonus of the "pass a structure of functions to everything for recursive calls" is that it makes it easy to parameterize the tactics on other things at the same time


Last updated: May 09 2021 at 21:10 UTC