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
Replying to
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.
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.
1
2
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
Show replies