Structure of mutual blocks generated by frontend

Stream: lean4

[Simon Dima]

I'm trying to understand what the mutual blocks sent to the compiler can look like after elaboration. For context, I'm aiming towards later converting the Lean definitions into a Rocq-style lambda-calculus with explicit mutual fixpoints. I'm working with the _unsafe_rec version of functions when available, and mostly not concerning myself with the specifics of elaborating mutual recursion to primitive recursors.

I know how to handle two classes of mutual blocks:

• There is exactly one definition in the block, and it is non-recursive
• There are one or more definitions in the block, all of which have a function type with at least one argument, and which are irreducibly mutually recursive (ie the dependency graph is strongly connected)

These two classes are not exhaustive, and I'm wary about there being examples which are in neither one; for example, if the following code was accepted by Lean, it would be such an example.

def K (_: α) (b: β): β := b

mutual
def a: Nat := K b 0
def b: Nat := K a 0
end

Are there situations in which Lean will send the compiler a mutual block containing > 1 definitions and in which at least one of the definitions does not have a function type? How artificial are these, is this an edge case or something which could plausibly come up in natural code?

[Mario Carneiro]

An easy example which does not fall into your categorization is one where the dependency graph is nontrivial but not an SCC:

mutual
def a: Nat := 37
def b: Nat := a
end

[Mario Carneiro]

This is compiled exactly as if the mutual was not there. Perhaps you would like to say "without loss of generality" you don't have to worry about this case

[Simon Dima]

From what I can see this sends two mutual blocks to the compiler, one defining a and one defining b, both singletons
Perhaps what I mean by "mutual block" is nonstandard terminology?

[Simon Dima]

I'm referring to what this comment calls a "block of functions to be compiled", not the syntactic mutual <decls> end construct (which is not visible after elaboration, as far as I can tell)

[Simon Dima]

That seems to be what the .all field of ConstantVal stores, and this comment calls that a mutual block

[Mario Carneiro]

I think all of those might be slightly different things

[Mario Carneiro]

are you interested in what the compiler sees or what is stored in the environment?

[Simon Dima]

I am very interested in whatever the differences between those two may be, but here I'm working with what is stored in the environment

[Mario Carneiro]

one reason they can be different is that anything noncomputable will not be sent to the compiler but will be in the environment

[Mario Carneiro]

Do you not care about unsafe mutual blocks?

[Mario Carneiro]

it seems easy enough to create non-function mutuals using unsafe

mutual
unsafe def a: Nat := b
unsafe def b: Nat := a
end

[Simon Dima]

Thanks! I do care about unsafe, I think, especially if there are practically relevant situations where we need it to use recursion to define non-functions.
Is absence of unsafe sufficient to guarantee that mutual definitions will be functions?

[Robin Arnez]

Not with well-founded recursion but certainly with partial_fixpoint:

mutual
def a : Nat := b partial_fixpoint
def b : Nat := a partial_fixpoint
end

And also, partial would be similar to unsafe although it creates opaque safe functions (with an unsafe implementation).