patternMinor
Meaning of the "why not" modality from linear type theory?
Viewed 0 times
meaningwhythelinearmodalitytheorytypefromnot
Problem
In linear type theory there is a modality written
According to ncatlab, there is a dual to this modality which is sometimes 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?Solution
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.
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.
Context
StackExchange Computer Science Q#105215, answer score: 2
Revisions (0)
No revisions yet.