mutual recursion

Stream: metaprogramming / tactics

[Reid Barton]

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?

[Reid Barton]

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

[Reid Barton]

and then tying the knot at the end

[Reid Barton]

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...

[Mario Carneiro]

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

[Reid Barton]

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?

[Mario Carneiro]

yes

[Reid Barton]

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

[Reid Barton]

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...

[Mario Carneiro]

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

[Reid Barton]

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