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
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
I usually ask for help when I over-extend myself in thinking about modal logic, and it's usually I'm speaking nonsense. I guess I was more thinking ‘later’ in the sense of ‘I have this modal operator for code that will be compiled later’, but that could be wrong.
My understanding is that there are many modal logics, each using ☐ and/or ◇ (and/or sometimes ◯) to mean different things. By social convention, in all of them ☐A -> A but not the converse, otherwise ☐ is a poor choice of name for whatever concept that logic models.
2
3
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