Does staged programming correspond to something like a ‘later’ modality? I'm wondering if you could flip things around, and use an ‘earlier’ modality to get something that looks a bit more like `constexpr`/`const fn`/`comptime` in C++, D, Rust, Zig, etc… 🤔
Conversation
I've always found that using a `Code` type for ‘later’ stuff (if that is indeed an acceptable way of looking at it) is a bit of a weird perspective outside of macros… but this is a familiarity thing? Would be kind of cool if both perspectives could interoperate somehow?
4
3
I suspect this'd correspond to monadic ('later') vs. comonadic ('earlier') modalities. Neel Krishnaswami & co. had a paper on a comonadic modality for purity in an impure language (I think you've seen it?), maybe something like that? Dunno if it'd work out for staging.
1
1
Replying to
Ahhh, I think I had it in Zotreo I think… was it “Recovering purity with comonads and capabilities”? Seems interesting, I can't remember having saved it tbh!