4
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks. I read that paper and I think I "get it" now: A ?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$ – Andrew Cann Mar 7 '19 at 6:57
  • $\begingroup$ I'm not 100% sure on that. ?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$ – Dan Doel Mar 7 '19 at 23:54
2
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Thanks. This is what I've been thinking lately and it occurred to me that ?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$ – Andrew Cann Jun 23 at 4:39
  • $\begingroup$ You are allowed to pull ?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$ – Rufflewind Jun 23 at 8:12
  • $\begingroup$ Are you sure? Looking at the sequent calculus rules on wikipedia and llwiki.ens-lyon.fr I can't see a way to derive ⊢ ?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$ – Andrew Cann Jun 23 at 10:57
  • $\begingroup$ Also I don't see why ?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$ – Andrew Cann Jun 23 at 11:08
  • $\begingroup$ (1) "From ⊢ Γ 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$ – Rufflewind Jun 27 at 20:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.