Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
In linear type theory there is a modality written ! where !T can be read as "infinite copies of T".
According to ncatlab, there is a dual to this modality which is sometimes written ?T and referred to as the "why not" modality. What is the meaning of this modality? How does ?T behave as a type?
First off, one thing I'd recommend is reading Filinski's Linear Continuations for ideas on how to interpret linear connectives (note, the ? modality got typeset as Γ in that for some reason).
In that paper, he uses the modality as part of the interpretation of call-by-name into linear logic. The idea is that you can kind of think of the non-modal types $T$ as being total, while $?T$ adds the possibility of divergence. If you want an analogue of "infinitely many copies of $T$", then it's, "zero or one $T$".
But of course, it's not like $1 + T$. It's more like a partiality monad living in an otherwise total language.
?T-typed expression can evaluate more or less than once, like a fork(), setjmp() or abort() call in C. A ?T-typed pattern/receiver can be written to as many times as you like. Also a !T can kinda be thought of as a memory cell or a data pointer, whereas a ?T can kinda be thought of as a jump/goto target or a code pointer. Does that all make sense? (I'm approaching from the perspective of a PL developer obviously).
$\endgroup$
Mar 7, 2019 at 6:57
?T is not like a label, I'd say. What it's like (for Filinski) is a delayed computation of a T which may never actually complete if you demand it. So, indeed, it may just abort(). I'm unsure about the forking. The other thing he gives to think about it is its encoding as ! which is like !(T ⊸ ⊥) ⊸ ⊥. So, you give it a T continuation (which is like a label) to jump to, but it is not obligated to actually call it. It also says it could be called twice, but it's not clear to me what that would mean in this interpretation.
$\endgroup$
From a resource interpretation,
If you receive a !T, you can extract as many copies of T as you need in your thread.
However, if you want to produce a !T, you need to be prepared to fulfill an unknown number of Ts in parallel, so whatever ingredients you use would need to be ! as well. If you have additional ⅋-threads to help you produce things, they would be ? since they might produce an unknown number of by products.
You can produce as many copies of T as you want in your thread and coalesce them all into a ?T.
However, if receive a ?T, you need to anticipate an unknown number of Ts arriving in parallel. Whatever ingredients you use would become ! and whatever you produce would also be afflicted with ? since you might produce arbitrary copies of them in parallel.
?T is sort-of like a bag/multiset of T. This would be nice since it gives a form of commutativity directly in the type system - the elements in the bag have to be processed in a way that's order-agnostic. It would also allow you to define Nat = ?1, and therefore define recursive/inductive types in terms of ?. However I can't seem to make this work. There's no way to construct an empty bag for instance, without assuming a ⊥. It also doesn't seem possible to define an eliminator for this Nat. Any thoughts?
$\endgroup$
Jun 23, 2020 at 4:39
?T out of thin air since ⊢ ?T. However, I don't think you can define a Nat-like eliminator because ?T "forgets" how many Ts exist inside.
$\endgroup$
Jun 23, 2020 at 8:12
⊢ ?T. From ⊢ Γ you can derive ⊢ Γ,?T, though you can also derive ⊥ that way. Also ?⊥ ⊢ ⊥, so this would allow you to pull ⊥ from thin air.
$\endgroup$
Jun 23, 2020 at 10:57
?T needs to forget how many T are in it - it needs to forget the "order" of the Ts, but I'm hoping I can define an eliminator for ?T / constructor for !T that allows counting the number of elements. Is there a logical reason why this is impossible? Thanks for your help btw :)
$\endgroup$
Jun 23, 2020 at 11:08
⊢ Γ you can derive ⊢ Γ,?T", thus you can always derive ⊢ ?T by setting Γ to an empty list. You can indeed pull ⊥ from thin air, since from Γ ⊢ Δ you can derive Γ ⊢ Δ, ⊥ (set Γ and Δ to empty lists). (2) I think the number of copies is a meta-property, inaccessible through the internal logic without perhaps extending LL with additional rules.
$\endgroup$
Jun 27, 2020 at 20:35