## Stream: metaprogramming / tactics

### Topic: mutual recursion

#### 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?

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

#### Reid Barton (Oct 18 2020 at 15:16):

and then tying the knot at the end

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

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

#### 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?

yes

#### Reid Barton (Oct 18 2020 at 16:05):

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

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

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

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