It occurs to me that there is the following interesting application of the dependent-type-theoretic formulation of the possibility/necessity modalities that, years ago, we wrote down in this entry (here).
Namely, to point out that when applied to linear dependent types, then the counit of the necessity modality as defined here embodies what in quantum information theory is a “measurement gate”.
Like so:
Let $\mathscr{H}$ be a linear type in the empty context, which is to be regarded as the Hlbert space of states that some quantum protocol is operating on. Think of the quantum teleportation-protocol as a good illustration in the following.
Now consider that in the process of the protocol, a measurement(-gate) is to be performed. Unwinding what the traditional song-and-dance boils down to, this means that
a set (a non-linear type) $R$ of measurement results is chosen.
a direct sum-decomposition
for an indexed set of direct summands $\mathscr{H}_\bullet = (r \mapsto \mathscr{H}_r)$
is chosen (with $\mathscr{H}_r$ consisting of those quantum states that one may find the system to have “collapsed” to after the result $r$ has been measured)
a quantum circuit is drawn whose gates may depend on $r : R$ (in the quantum teleportation protocol as shown here, this dependency is through the variable called $\sigma$ there)
As a result, quantum circuits that include measurement gates are actually fiberwise morphisms in a category of bundles of Hilbert spaces over finite sets of (potential) classical outcomes.
Traditional literature never puts it this way (some texts on Quipper get close, but I haven’t seen it stated real clearly there, either), but it is clear from inspection that this is what happens.
Now one should ask: In this dependent-linear-typed picture of quantum information protocols: What is a measurement gate itself?
To see this, observe that for a finite index set of results $R$, the direct sum of result Hilbert space is equivalently their categorical product, hence their limit, hence their right base change along $R \to \ast$:
To put this into the context of possible measurement results, context-extent it to $R$ (which I’ll denote by $R^\ast$, if you allow) to get
Now the collapse postulate of quantum physics says that if we are in context $r$ then a measurement operates on quantum states as the linear projection $p_{r} \colon \mathscr{H} \xrightarrow{\;} \mathscr{H}_r$ on its $r$th direct summand.
But, as a linear map dependent on $r$, this is just the $(R^\ast \dashv \underset{r : R}{\prod})$-counit
(!)
So if $\Box \,:=\, R^\ast \circ \underset{r : R}{\prod}$ denotes the corresponding comonadic modility (“necessarily so in possible worlds $R$”), then we discover that a quantum measurement gate with possible outcomes $\mathscr{H}_\bullet$ indexed by $R$, understood as an $R$-dependent linear map, is the necessity counit
That seems kind of cute.
For example, in the quantum teleportation protocol, this would be Alice’s measurement, and then Bob would go and do $r : R \;\vdash\; \sigma_r : \mathscr{H}_r \xrightarrow{\;\;} \mathscr{H}_r$ to get
As it goes with these Yoneda-like insights, it’s all locally trivial, but this looks like the right picture to make explicit:
Q: What is a quantum measurement gate seen in dependent linearly typed quantum programming languages?
A: The necessity counit on the dependent type of possible outcomes.
Last revised on September 28, 2022 at 08:00:28. See the history of this page for a list of all contributions to it.