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.
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
Modal logics like K, KD, KB, K4, don't have []A -> A (or the converse). One way to think of it: []A says that A is required. But not all kinds of requirements are always met!
1
2
In this diagram, a modal logic includes []A -> A iff it has a path from it to T
read image description
ALT
1
3
I tend to think of the box/diamond divide as more closely related to conjunction and disjunction: for a modal operator O, having O(A & B) <-> (OA & OB) is a box-like quality, and having O(A v B) <-> OA v OB is a diamond-like quality
1
2
I need to think about this more, and try to translate it into examples I know from programming, but this seems like a very useful way of thinking about it. Thanks so much!
1
2
Seems like Rust's references can't go in the opposite direction of the iff, as you'd need to return a reference to a temporary variable! :( play.rust-lang.org/?version=stabl
I'd I'm reading that right, you've got O(A & B) -> (OA & OB) and O(A v B) -> (OA v OB) both, but neither converse. Is that right?
1
Correct!
1
1
Show replies