This is cool, I have been working on something similar with Lean4 albiet focused on compiling to Substrait

This is pretty well done as well https://github.com/palladin/lean-linq