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
Replying to
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
Replying to
Yeah. And the Core Calculus of Dependency paper used a monad to track binding time which i think is related to constants.
2
Replying to
Is "later" sometimes spelled "box"? I'm involved with a language which uses (contextual) box types for staged programming, and we've long been wondering how to add the corresponding diamond modality, maybe this is it?
1
2
I'm not sure actually! In hindsight I could have been using the term ‘later modality’ imprecisely… I *think* box and diamond can take on different meanings depending on your perspective? Far from an expert, alas.
1
1
Show replies
Replying to
Presuming you know Davies-Pfenning "A modal analysis of staged computation"?
1
3
Yeah! I think I forgot how these were related! I have a feeling I'd got my head around this before, and then forgot?
Quote Tweet
Replying to @haskell_cat and @davewripley
Yeah, that seems right! I guess that interpretation could match up with staged programming, in terms of being able to splice/run `Code A`s, to get an `A`? That *does* actually feel like constexpr the more I think about it! 
1
1
Show replies