Generics and containers in Lean

Stream: lean4

[Guilherme Silva]

Does Lean have a library for containers like this one in Idris (https://github.com/idris-lang/idris2/blob/master/libs/contrib/Data/Container.idr)? Containers are one way to give more type information for Expressions.
They can be useful to do some kind of generics metaprogramming (https://github.com/effectfully/Generic), like deducing Equality for vectors.

[Mario Carneiro]

This looks a bit like our work on W types in lean 3: http://www.contrib.andrew.cmu.edu/~avigad/Papers/qpf.pdf

[Jannis Limperg]

I haven't seen a container library for Lean, but you should be able to copy the Idris stuff more or less verbatim. Some notes that may or may not be helpful:

• The containers implemented there are non-indexed, so they can represent only non-indexed inductive types. For indexed inductive types, you need indexed containers. The Agda stdlib has these.
• You need funext to prove anything about containers, but I guess that's not a problem in Lean.
• The runtime representation of a containerised data type is not very efficient because there are functions everywhere.
• Programming directly with containerised types is syntactically cumbersome. It can be done, but you'd probably want a metaprogram that translates back and forth between your types and their containerised versions.

[Mario Carneiro]

I'm interested in using this a la deriving Generic in order to get easy proofs of finiteness, countability, and other things given only instances on built in types like sum, sigma and W. But the approach is definitely algorithmically suboptimal, so when performance is a concern it's probably better to write the derive handler directly