Conversation

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.

cybersyx

@cyberglot

this sounds like nanopass. but than the first thing you said sounds like partial evaluation.

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.

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.

cybersyx

@cyberglot

do you have any papers about this? I'm interested

Software engineering demands generality and abstraction, performance demands specialization and concretization. Generative programming can provide both, but the effort required to develop high-qual...

sciencedirect.com/science/articl is the classic MetaML paper and infoscience.epfl.ch/record/150347 is great on LMS.

infoscience.epfl.ch

Acm Sigplan Notices

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 :-)

cybersyx

@cyberglot

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 🙌🏽

Brendan Zabarauskas

@brendanzab

10:40 AM · Oct 22, 2021Twitter Web App

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.

Replying to

IIUC combining staging with DTT is still a bit tricky though?

Replying to

I think this is the best one we have so far:

Quote Tweet

Jacques Carette

@jjcarett2

· Sep 26, 2021

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.

Replying to

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?