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.

$\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 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 at 23:54

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.