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.
Conversation
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'm sure I forgot 90% of the answer, but a key question is "how much staging" — everybody implements their universe construction and well-formed expressions (Type T and Exp T), but how much of the language do you want to cover?
3
1
Not sure I understand the bit about “Type T and Exp T”, but I'd probably answer “as much as possible”, but I'm annoyingly greedy and demanding 😅
2
"Type T" was a sloppy shortcut for universe constructions, and the other was the usual indexed Exp : Set -> Set that you’d find in an Agda tutorial or a McBride greeting… Either you’ve seen those, or you can google them, or I’m being unclear…
1
2
Yeah, might need to do some looking. Is `Exp : Set -> Set` similar to `el : tp -> sort`, that you might find in LF descriptions of type theory? Eg. homotopytypetheory.org/2014/06/08/hir – I'm guessing not?