Use staging for performance?

[clayrat]

This is more of a feature request, of course :)

https://mpickering.github.io/papers/staged-sop.pdf Pickering, Loeh, Wu, [2020] "Staged Sums of Products"

https://kosmikus.org/StagedSOP/staged-sop-haskell-symposium-talk.pdf

[clayrat]

Also this seems to overlap with the recent research of @gallais et al on Frex, though I'm not sure what stage (:wink:) that work is at.

[stefan-hoeck]

I have looked at those SOP articles before, but only superficially. I'm not sure, however, whether we have the necessary metaprogramming machinery for that in Idris2. Do you have any hints in that direction? Thanks anyway for the articles. The Frex one is new to me.