I mainly want this for dependently typed metaprogramming, levitation, and faster codegen, but yeah, having it for proofs would be really cool too.
Conversation
OTOH...
"I want staging"
Mom: "we have staging at home"
Staging at home: Coq's "Eval cbv in <term>"
1
2
"I want staging"
Mum: "we have staging at home"
Staging at home: `const fn foo<const x: Int>() -> T { ... }`
1
2
not sure I get what staging means here? would you mind explaining? 😅
1
(I have a metaprogramming project going at $dayjob and if it's a concept I'm not familiar with, I'd like to know more)
1
TBH I need to understand more about it, but here I think you can consider it's a bit of code that is 'staged'. ie. it won't be compiled until you provide it with a constant argument.
1
I do believe there might be a connection between 'staged programming' and Rust's 'angle bracket' parameters (which are always monomorphised), but I'm not really sure of the precise connection. There's a bibliography of related stuff here:
3
1
1
Was also wondering about this stuff here:
Quote Tweet
Has there been any work on looking at the relationship between monomorphised, static polymorphism (like in C++ and Rust, etc), and staged programming? I think the interesting thing here is that instead of inlining stuff, we sort of memoize each instantiation?
Show this thread
1
1
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.
1
this sounds like nanopass. but than the first thing you said sounds like partial evaluation.
2
1
Yeah I think(?) the difference with nanopass is that you are going between multiple different languages. Where as with multistage programming you are in the same language… or something?