using this style of generic programming in other languages

[GunpowderGuy]

Hello, i am idris2 programmer ( considering moving to lean 4 ) that wonders whether "Practical generic programming over a universe of native datatypes" can be applied to either of those languages.

Idris2 specially would benefit from this since reflection meta-programming is less integrated with actual programming than in lean4

I apologize in advance if this isnt the place for such a high level question

[GunpowderGuy]

@flupe @gallais What do you think?

[gallais]

I already do something somewhat similar in base: instead of deriving functions directly by analysing the
type, I start by computing a view of it that is known to be amenable to automatically deriving the thing I
am interested in. For instance, this inductive type in Deriving.Functor:

https://github.com/idris-lang/Idris2/blob/04c5531d9bf95f2a02cb4d74b6594390d565b6b9/libs/base/Deriving/Functor.idr#L79-L87

You could instead have a clean HasDesc interface and derive instances for it. Of course the advantage of
rolling out your own representation is that it can be ad-hoc for the property you care about. Not all functors
are traversable and so if you are going to reuse the same universe you will need to carve out appropriate
subsets.