There is 'multistage programming' where programs are broken up into multiple stages of code generation - kind of like type-safe macros. Here we just have compile time and runtime so I was referring to it as 'staging'. But yeah I could have no idea what I'm talking about.
Conversation
this sounds like nanopass. but than the first thing you said sounds like partial evaluation.
2
1
If you see that, this definition might help: Staging is partial evaluation _minus_ binding-time analysis:
instead of letting inference _guess_ what is static and what is dynamic, and tweaking the program till the result is right, you drop the inference and use types.
3
5
Somewhat unusually, there seems to be consensus that staging beats inference; so much so that Scala 3's macro system/inliner/optimizer is actually based on a novel variation of staging.
1
3
do you have any papers about this? I'm interested
2
1
sciencedirect.com/science/articl is the classic MetaML paper and infoscience.epfl.ch/record/150347 is great on LMS.
1
4
Last, Kiselyov's okmij.org/ftp/meta-progr page is also a great buffet of super-insightful pearls on staging and metaprogramming — picking is hard but it's worth browsing :-)
1
5
thank you so much for the references, I'm starting to research metaprogramming (from a DTT point of view) and those references is going to unbiase me 🙌🏽
2
1
Yeah, I'd love to see this somehow combined with stuff like levitated datatypes at some stage (as in The Gentle Art of Levitation)… I think that could be really cool.
1
IIUC combining staging with DTT is still a bit tricky though?
2
I think this is the best one we have so far:
Quote Tweet
Replying to @andrasKovacs6 and @brendanzab
I'm in favour of that stance. The most interesting work wrt staging & dependent types that I know is Igarashi's link.springer.com/chapter/10.100 (also on arxiv).
I'd say that 's work on multi-stage programming in 2LTT will handily surpass that. At least, I'm very optimistic.
3