RFC: mutual structures

[ice1000]

Proposal

I think structures should work in mutual blocks. #2587 reports an error message related to this feature, and everyone commented in the issue expected this to work (I expect this to fulfill the "community feedback" requirement), but the issue is closed as it's not about making it work.

A simple example use case can also be found in #2587.

Impact

Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[arthur-adjedj]

Lean (kernel included) considers an inductive type to be "structure-like" iff it is non-recursive, not indexed, and has a single constructor. Because structure types benefit from special treatments such as having primitive projections and eta-conversion, it would be unwise to blindly adopt that RFC. In particular, eta-conversion on recursive/mutual structures can lead to a form of undecidability of defeq that's quite hard to deal with.

One possibility to handle this feature would be to allow the structure syntax to construct inductive types which are not structure-like. This would require no change to the kernel. However, such "structure but not structure-like" types would lose both eta-conversion and primitive projections, and would only really benefit from having the notations that are exclusive to structures such as {foo := ...}. I am not certain of the added benefits of this feature, but I am all for having better error messages when using structures in mutual blocks.

[nomeata]

I felt silly once having had to write the projection functions for a almost-structure (it was recursive) by hand because I couldn't see structure syntax, so I think there is some added benefit.

[arthur-adjedj]

Perhaps Lean could benefit from dissociating between structures and non-recursive structures then, including in the kernel. In particular, a recursive structure , could still benefit from having primitive projections, which are great for performance, without having eta-conversion.

[ice1000]

@arthur-adjedj can you enlighten me on how does structure eta conversion gets undecidable?

[arthur-adjedj]

Also, I believe some lean libraries already offer a way to automatically generate "projections" on non-structures, notably this one

[arthur-adjedj]

@arthur-adjedj can you enlighten me on how does structure eta conversion gets undecidable?

Consider the following (recursive) structure:

structure Foo where
  foo : Foo

When comparing two arbitrary neutral terms, i.e variables x =?= y : Foo. The type-checker might want to eta-expand those values recursively, checking against x.1 =?= y.1 : Foo, then x.1.1 =?= y.1.1, so on and so fourth. Two things to note:

• Such eta-expansion on i.e variables can be desirable. A (proof-relevant) structure might only contain proof-irrelevant fields for example

• I don't think such an infinite loop would trigger in Lean in practice currently. Because conversion is untyped in the system, Lean has no way to trigger eta-conversion on two neutrals, and only triggers it when one of the two sides is already built from the constructor. All I am arguing is that eta on recursive records is tricky/non-trivial to handle, and might not be necessarily worth the risk.

  I believe Agda supports recursive records, as well as eta-expansion, and also uses typed conversion, which allows it to eta-expand neutrals. Does anyone know how it handles this issue ?