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?
Conversation
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
1
2
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
To elaborate on why the inverse breaks, Rust allows you to return references to data behind a reference you passed as an argument, but you can't:
- package some referenced data inside another reference without copying
- return reference to temporary memory
1
1
Hmm. Then I don't know of any modal logic that exhibits this kind of behaviour! Maybe or or or does?
1
4
Show replies