nLab function monad

Contents

Context

Categorical algebra

Mapping space

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

In a cartesian closed category/type theory 𝒞\mathcal{C}, given any object/type BB there is a monad

Maps(B,):𝒞𝒞 Maps(B,-) \colon \mathcal{C} \to \mathcal{C}

given by forming the internal hom out of BB, hence the “space of functions” out of BB. This is sometimes called the function monad. Its unit is given by sending values to constant functions with that value, and the monad operation is given by evaluating on the diagonal.

In the context of monads in computer science this monad is called the reader monad or environment monad. It serves to write programs in which all operations may “read in” a state of type BB (an “environment” variable).

Definition

We first describe the reader monad explicitly

as a monad on 𝒞=\mathcal{C} = Sets.

Then we describe it, more generally as the monad induced by a right base change adjunction

In this form the construction makes sense more generally (see for instance the quantum reader monad).

We write

Maps(,):𝒞 op×𝒞𝒞 Maps(-,-) \;\colon\; \mathcal{C}^{op} \times \mathcal{C} \longrightarrow \mathcal{C}

for the corresponding internal hom. In Sets this is the operation of forming function sets.


Fix B𝒞B \in \mathcal{C}.

In components

  1. The underlying-functor of the BB-reader monad is

    B:DMaps(B,D). \bigcirc_B \;\colon\; D \;\mapsto\; Maps(B,D) \,.
  2. The unit of the monad is given by constructing constant functions:

    D η D B Maps(B,D) d (bd)=const d \begin{array}{ccc} D & \xrightarrow{ \;\; \eta^{\bigcirc_B}_D \;\; } & Maps(B,D) \\ d &\mapsto& \big( b \;\mapsto\; d \big) \mathrlap{ \;=\; const_d } \end{array}
  3. The monad multiplication is given by “evaluating diagonally:

    Maps(B,Maps(B,D)) μ B Maps(B,D) f()() (bf(b)(b)). \begin{array}{ccc} Maps\big( B ,\, Maps(B,D) \big) &\xrightarrow{\;\;\; \mu^{\bigcirc_B} \;\;\;}& Maps(B,D) \\ f(-)(-) &\mapsto& \big( b \;\mapsto\; f(b)(b) \big) \mathrlap{\,.} \end{array}

To check that this definition satisfies the monad-axioms:

unitality:

Maps(B,D) η Maps(D,B) B Maps(B,Maps(B,D)) μ D B Maps(B,D) (bf(b)) (b(bf(b))) (bf(b)) \begin{array}{ccc} Maps(B,D) &\xrightarrow{\;\;\; \eta^{\bigcirc_B}_{Maps(D,B)} \;\;\;}& Maps\big( B, Maps(B,D) \big) &\xrightarrow{\;\;\; \mu^{ \bigcirc_B }_{D} \;\;\;}& Maps(B,D) \\ \big( b' \mapsto f(b') \big) &\mapsto& \Big( b \mapsto \big( b' \mapsto f(b') \big) \Big) &\mapsto& \big( b \mapsto f(b) \big) \end{array}

and

Maps(B,D) Maps(B,η D B) Maps(B,Maps(B,D)) μ D B Maps(B,D) (bf(b)) (b(bf(b))) (bf(b)) \begin{array}{ccc} Maps(B,D) &\xrightarrow{\;\;\; Maps\big( B, \eta^{\bigcirc_B}_{D} \big) \;\;\;}& Maps\big( B, Maps(B,D) \big) &\xrightarrow{\;\;\; \mu^{ \bigcirc_B }_{D} \;\;\;}& Maps(B,D) \\ \big( b \mapsto f(b) \big) &\mapsto& \Big( b \mapsto \big( b' \mapsto f(b) \big) \Big) &\mapsto& \big( b \mapsto f(b) \big) \end{array}

associativity:

Maps(B,Maps(B,Maps(B,D))) μ Maps(B,D) B Maps(B,Maps(B,D)) μ D B Maps(B,D) (b(b(bf(b,b,b)))) (b(bf(b,b,b))) (bf(b,b,b)) \begin{array}{ccc} Maps\Big( B, Maps\big(B, Maps(B,D) \big) \Big) &\xrightarrow{\;\;\; \mu^{\bigcirc_B}_{ Maps(B,D) } \;\;\;}& Maps\big(B, Maps(B,D) \big) &\xrightarrow{\;\;\; \mu^{\bigcirc_B}_{ D } \;\;\;}& Maps(B,D) \\ \Big( b \mapsto \big( b' \mapsto (b'' \mapsto f(b, b', b'')) \big) \Big) &\mapsto& \big( b' \mapsto (b'' \mapsto f(b', b', b'')) \big) &\mapsto& \big( b'' \mapsto f(b'', b'', b'') \big) \end{array}

and

Maps(B,Maps(B,Maps(B,D))) Maps(B,μ D B) Maps(B,Maps(B,D)) μ D B Maps(B,D) (b(b(bf(b,b,b)))) (b(bf(b,b,b))) (bf(b,b,b)) \begin{array}{ccc} Maps\Big( B, Maps\big(B, Maps(B,D) \big) \Big) &\xrightarrow{\;\;\; Maps\big( B, \mu^{\bigcirc_B}_{ D } \big) \;\;\;}& Maps\big(B, Maps(B,D) \big) &\xrightarrow{\;\;\; \mu^{\bigcirc_B}_{ D } \;\;\;}& Maps(B,D) \\ \Big( b \mapsto \big( b' \mapsto (b'' \mapsto f(b, b', b'')) \big) \Big) &\mapsto& \big( b' \mapsto (b'' \mapsto f(b', b'', b'')) \big) &\mapsto& \big( b'' \mapsto f(b'', b, b) \big) \end{array}

Via base change

For BSetsB \in Sets, write 𝒞 B\mathcal{C}_B for the category of BB-indexed sets (D b) b:B(D_b)_{b \colon B} of objects of 𝒞\mathcal{C}. (More generally, if 𝒞\mathcal{C} is a locally cartesian closed category (categorical semantics for dependent type theory), take 𝒞 B\mathcal{C}_B be the slice category over BB.)

The right base change adjunction (context extension \dashv dependent product) is

𝒞 B (p B) *= B(p B) * 𝒞 (D b) b:B b:BD b \begin{array}{ccc} \mathcal{C}_B & \underoverset {\underset{(p_B)_\ast = \prod_{B}}{\longrightarrow}} {\overset{ (p_B)^\ast }{\longleftarrow}} {\;\;\; \bot \;\;\;} & \mathcal{C} \\ (D_b)_{b \colon B} &\mapsto& \prod_{b \colon B} D_b \end{array}

Under the evident identification of maps f:BDf \colon B \to D with tuples (f(b)) b:B\big( f(b) \big)_{b \colon B}, the reader monad is the monad induced from this adjunction:

B(p B) *(p B) *. \bigcirc_B \;\simeq\; (p_B)_\ast (p_B)^\ast \,.

Remark

One may also think of this as being the polynomial functor associated with this span:

*B**. \ast \leftarrow B \rightarrow \ast \rightarrow \ast \,.

Remark

The comonad obtained by composing the other way around, (p B) *(p B) *(p_B)^\ast (p_B)_\ast, is the modal operator usually called necessity

From the universal property of the Cartesian product, one finds that:

The adjunction unit is

b:B D id D D D η D B b:BD d (d,,d) \begin{array}{ccc} b \colon B \; \vdash \; & D &\xrightarrow{\;\;\; id_D \;\;\;}& D \\ && \updownarrow \\ & D &\xrightarrow{\;\;\; \eta^{ \bigcirc_B }_D \;\;\;}& \prod_{b \colon B} D \\ & d &\mapsto& (d, \cdots, d) \end{array}

The adjunction counit is:

b:BD b id b:BD b b:B b:BD b ϵ D B D b (d b) b:B d b \begin{array}{ccc} & \prod_{b' \colon B} D_{b'} &\xrightarrow{\;\;\; id \;\;\;}& \prod_{b' \colon B} D_{b'} \\ && \updownarrow \\ b \colon B \;\dashv\; & \prod_{b' \colon B} D_{b'} &\xrightarrow{\;\;\; \epsilon^{ \star_B }_D \;\;\;}& D_{b} \\ & (d_{b'})_{b' \colon B} &\mapsto& d_{b} \end{array}

The adjunction unit is clearly the monad unit.

The adjunction counit gives the multiplication on the monad:

b:B(p B) * b:B(p B) *D b:B(ϵ B)(p B) * b:B(p B) *C ((f b) b) b,b:B ((f b) b) b:B \begin{array}{ccc} \prod_{b \colon B} (p_B)^\ast \prod_{b' \colon B} (p_B)^\ast D &\xrightarrow{\;\;\; \prod_{b \colon B} \big( \epsilon^{\star_B} \big) (p_B)^\ast \;\;\;}& \prod_{b' \colon B} (p_B)^\ast C \\ \big( (f_{b'})_{b} \big)_{b', b \colon B} &\mapsto& \big( (f_{b})_{b} \big)_{b \colon B} \end{array}

Properties

Relation to coreader- and state monad

In a cartesian closed category/type theory 𝒞\mathcal{C}, the reader monad [B,]:𝒞𝒞[B,-] \colon \mathcal{C}\to \mathcal{C} is right adjoint to the coreader comonad B×()B\times (-).

The composite of coreader comonad followed by reader monad is the state monad [B,B×()][B,B \times (-)] This monad models the situation where a program may not only depend on a immutable parameter b:Bb \colon B but may be allowed to change it.

Just as the coreader comonad canonically becomes a monad when BB is a monoid, so the reader monad becomes a comonad in that case, and then it is sometimes called the “traced comonad”.

Relation to random variables in probability theory

It makes sense to think of [B,][B,-] as producing spaces of random variables (Verdier 14) depending on possible worlds bBb \in B [Toronto & McCarthy 10b, slide 24].

(While, from the perspective of modal type theory, its siblings W * WW^\ast \prod_W and W * WW^\ast \sum_W may be called necessity and possibility, respectively).

The intuition behind the Reader monad, for a mathematician, is perhaps stochastic variables. A stochastic variable is a function from a probability space to some other space. So we see a stochastic variable as a monadic value. [Verdier 14]

you could interpret this by regarding random variables as reader monad computations. [Toronto & McCarthy 10b, slide 35]

Toronto & McCarthy 10a, 2.2, Toronto 14, 6.2 call the function monad the random variable idiom.

This is also brought out by the relation of linear reader algebras to quantum measurement, see below. For more see also at nondeterministic computation the section Via indefiniteness effects.

Free modules over the reader monad

For BB a set, the Kleisli category for the BB-reader monad has BB-tuples of functions as morphisms:

(On the left we are showing the situation of the comparison functor and on the right we are using the “bind”-notation from monads in computer science.)

General modules over the reader monad

The reader monad on Set (and similar) does not generally arise from a monadic adjunction and its general algebras may not be easily characterizable. (See also MO:a/868317.)

A special case is when WW is a 2 element set, where the WW-reader algebras on SetSet correspond to idempotent semigroups, also known as rectangular bands.

But the definition of the reader monad makes sense also for other hyperdoctrines such as for dependent linear types: For the resulting “linear” or “quantum” version of the reader monad the situation is different, see below.

Examples

Quantum reader monad

As remarked above, while the BB-reader monad on toposes such as Set is induced from the base change adjunction as B()B(B×())\bigcirc_B(-) \,\coloneqq\, \underset{B}{\prod} \big( B \times (-) \big), the functor B:Set /BSet\underset{B}{\prod} \;\colon\; Set_{/B} \xrightarrow{\phantom{--}} Set is not in general a monadic functor, so that BB-reader-algebras are not in general equivalent to BB-indexed sets.

However, this situation changes for BB-readers analogously defined in other hyperdoctrines.

We discuss the example of the reader monad induced by BB-dependent linear types which have biproducts, such as BB-indexed sets of vector spaces (these we may think of as “quantum reader monads”, see the discussion at Quantum Modal Logic). We follow CQTS (2022):

Proposition

(quantum B\bigcirc_B-algebras are BB-dependent linear types)
For BB \;\in\; FiniteSets, the category of algebras for the BB-reader monad

B: Vect Vect Maps(B,)b:B \array{ \bigcirc_B \colon & Vect &\xrightarrow{\phantom{---}}& Vect \\ & \mathscr{H} &\mapsto& Maps\big(B, \mathscr{H} \big) \mathrlap{ \; \simeq \; \underset{b \colon B}{\bigoplus} \mathscr{H} } }

on the category Vect of vector spaces (over any given ground field) is equivalent to that of vector bundles over BB (hence to BB-indexed sets of vector spaces):

EM( B)Vect B. EM\big( \bigcirc_B \big) \;\;\simeq\;\; Vect_B \,.

Proof

We state first an abstract proof and then a concrete proof.

Abstractly, observe that Vect has (finite) biproducts (given by the direct sum of vector spaces) which together with the assumption that BB is finite implies that B:Vect BVect\underset{B}{\prod} \;\colon\; Vect_B \xrightarrow{\;} Vect:

  1. is not only a right adjoint but also a left adjoint (hence an ambidextrous adjoint to pullback of vector bundles along B*B \to \ast), hence in particular it preserves all colimits;

  2. is a conservative functor (since the BB-components of any morphism of vector bundles over VV can still be extracted via (co-)projections from their image under forming the biproduct over BB).

Therefore the conditions for the monadicity theorem are met (see there), implying that the functor is monadic functor, which in turn implies the claim.


Alternatively, we now check the claim more concretely by unwinding what it means for a vector space to carry B\bigcirc_B-algebra structure and for a linear map between vector spaces to be a homomorphism for this structure:

First observe that the B\bigcirc_B-monad product μ: B Bμ B\mu \;\colon\; \bigcirc_B \bigcirc_B \xrightarrow{\mu} \bigcirc_B on a vector space Vect\mathscr{H} \,\in\, Vect is explicitly given by:

b:Bb:B μ b:B (ψ b,b) b,b:B (ψ b,b) b:B \array{ \underset{b \colon B}{\bigoplus} \; \underset{b' \colon B}{\bigoplus} \; \mathscr{H} & \xrightarrow{\;\; \mu^{\bigcirc}_{\mathscr{H}} \;\;} & \underset{b'' \colon B}{\bigoplus} \mathscr{H} \\ \big( \psi_{b,b'} \big)_{b,b' \colon B} &\mapsto& \big( \psi_{b'' ,b''} \big)_{b'' \colon B} }

and that a B\bigcirc_B-algebra structure on \mathscr{H} is a linear map of this form:

(1)ρ :b:B(P b) b:B. \rho^\bigcirc_{\mathscr{H}} \;\colon\; \underset{b \colon B}{\oplus} \mathscr{H} \xrightarrow{\phantom{-}(P_b)_{b \colon B}\phantom{-}} \mathscr{H} \,.

Of such maps, the B\bigcirc_B-action property (here) demands that the following two linear maps are equal:

b:Bb:B μ b:B ρ (ψ b,b) b,b:B (ψ b,b) b,b:B b:BP b(ψ b,b) and b:Bb:B ρ b:B ρ (ψ b,b) b,b:B (b:BP b(ψ b,b)) b:B b,b:BP b(P b(ψ b,b)). \array{ & \underset{b \colon B}{\bigoplus} \; \underset{b' \colon B}{\bigoplus} \; \mathscr{H} &\xrightarrow{\; \mu^\bigcirc_{\mathscr{H}} \;}& \underset{b'' \colon B}{\bigoplus} \mathscr{H} &\xrightarrow{\; \rho^\bigcirc_{\mathscr{H}} \;}& \mathscr{H} \\ & \big( \psi_{b,b'} \big)_{b,b' \colon B} &\mapsto& \big( \psi_{b'',b''} \big)_{b'',b'' \colon B} &\mapsto& \underset{b'' \colon B}{\sum} P_{b''}(\psi_{b'',b''}) \\ \text{and} & \\ & \underset{b \colon B}{\bigoplus} \; \underset{b' \colon B}{\bigoplus} \; \mathscr{H} &\xrightarrow{\; \bigcirc \rho^\bigcirc_{\mathscr{H}} \;}& \underset{b'' \colon B}{\bigoplus} \mathscr{H} &\xrightarrow{\; \rho^\bigcirc_{\mathscr{H}} \;}& \mathscr{H} \\ & \big( \psi_{b,b'} \big)_{b,b' \colon B} &\mapsto& \big( \underset{b \colon B}{\sum} P_{b}(\psi_{b,b'}) \big)_{b' \colon B} &\mapsto& \underset{b, b' \colon B}{\sum} P_{b'}\big(P_{b}(\psi_{b,b'})\big) \mathrlap{\,.} }

By considering the value of these maps on tuples of vectors (ψ b,b) b,b:B\big(\psi_{b,b'}\big)_{b,b' \colon B} which are non-zero only for single elements (b,b)B×B(b,b') \in B \times B one finds that the above condition is equivalent to the following condition:

b,b:BP bP b={P b ifb=b 0 otherwise. \underset{ b, b' \colon B }{ \forall } \;\;\;\; P_b \circ P_{b'} \;=\; \left\{ \array{ P_b &\text{if} \; b = b' \\ 0 & \text{otherwise} \,. } \right.

Moreover, the B\bigcirc_B-unit idη B B\id \xrightarrow{\;\; \eta^{\bigcirc_B} \;\;} \bigcirc_B is given by the diagonal map into the biproduct

η B b:B ψ (ψ bψ) b:B \array{ \mathscr{H} &\xrightarrow{\;\; \eta^{\bigcirc_B}_{\mathscr{H}} \;\;} & \underset{b \colon B}{\bigoplus} \mathscr{H} \\ \psi &\mapsto& (\psi_b \coloneqq \psi)_{b \colon B} }

so that the unitality property (here) of the B\bigcirc_B-algebra structure (P b) b:B(P_b)_{b \colon B} demands equivalently that the composite

η B b:B ρ B ψ (ψ) b:B b:BP b(ψ) \array{ \mathscr{H} &\xrightarrow{\; \eta^{\bigcirc_B}_{\mathscr{H}} \;}& \underset{b \colon B}{\bigoplus} \mathscr{H} &\xrightarrow{\; \rho^{\bigcirc_B}_{\mathscr{H}} \;}& \mathscr{H} \\ \psi &\mapsto& \big( \psi \big)_{b \colon B} &\mapsto& \underset{b \colon B}{\sum} \; P_b(\psi) }

is the identity function on \mathscr{H}, hence that this system of projection operators is “complete” in that

b:BP b=id . \underset{b \colon B}{\bigoplus} P_b \;=\; id_{\mathscr{H}} \,.

In summary, this means that for BB-tuples of linear maps (P b:) b:B(P_b \colon \mathscr{H} \to \mathscr{H})_{b \colon B} as in (1) to constitute a B\bigcirc_B-module structure is equivalent to them being systems of orthogonal linear projection operators, whose images

bim(P b) \mathscr{H}_b \;\coloneqq\; im(P_b) \;\subset\; \mathscr{H}

span\; \mathscr{H} under direct sum:

b:B b. \mathscr{H} \;\simeq\; \underset{b \colon B}{\bigoplus} \mathscr{H}_b \,.

Such structures, of course, are exactly the images under the right base change B:Vect BVect\underset{B}{\prod} \;\colon\; Vect_B \longrightarrow{\;} Vect of BB-indexed sets of vector spaces.

Finally, the homomorphism-property on a linear map ϕ\mathscr{H} \xrightarrow{\phi} \mathscr{H}' between the underlying vector spaces of two such B\bigcirc_B-modules demands that the following diagram commutes:

b:B b:B b:B (P b) b:B (P b) b:B ϕ . \array{ \underset{b \colon B}{\bigoplus} \mathscr{H} &\xrightarrow{\;\;\; \underset{b \colon B}{\oplus} \;\;\;}& \underset{b \colon B}{\bigoplus} \mathscr{H} \\ \mathllap{ {}^{ \big( P_b \big)_{b \colon B} } } \big\downarrow && \big\downarrow \mathrlap{ {}^{ \big( P'_b \big)_{b \colon B} } } \\ \mathscr{H} & \underset{\phantom{---} \phi \phantom{---} } {\longrightarrow} & \mathscr{H}' \,. }

The BB-indexed components of this condition require that ϕ\phi commutes with all these projection operators, in that

b:BP bϕ=ϕP b. b \colon B \;\;\;\; \vdash \;\;\;\; P'_b \circ \phi \;=\; \phi \circ P_b \,.

But this evidently means that ϕ\phi itself is the image under the direct sum-functor

ϕ=b:ϕ b \phi \;=\; \underset{b \colon}{\oplus} \phi_b

of a BB-tuple of linear maps between the BB-indexed component spaces:

b:B: b. b \colon B \;\;\; \colon \;\;\; \mathscr{H}_b \longrightarrow \mathscr{H}' \,.

This is the defining property of morphisms in Vect BVect_B and hence shows that B\bigcirc_B-algebra homomorphisms are equivalently morphisms of BB-indexed sets of vector spaces, hence that the two categories are agree.

Example

(free quantum B\bigcirc_B-algebras and quantum measurement bases)
The free B\bigcirc_B-algebras in Vect are those whose underlying vector space is of the form B=b:B\bigcirc_B \mathscr{B} = \underset{b \colon B}{\bigoplus} \mathscr{B} for any Vect\mathscr{B} \,\in \, Vect, hence, under the equivalence of Prop. , are those BB-dependent linear types which happen to assign the same vector space \mathscr{B} for all b:Bb \colon B.

But homomorphisms of such free B\bigcirc_B-algebras are still allowed to be non-trivially BB-dependent families of linear maps. This is directly a special case of Prop. but is also immediate under the Kleisli equivalence from observing that B\bigcirc_B-Kleisli morphisms are of the following form:

(ϕ b) b:B b:B. \array{ \mathscr{B} &\xrightarrow{ \big( \phi_b \big)_{b \colon B} }& \underset{b \colon B}{\bigoplus} \mathscr{B}' \,. }

In quantum information theory the B\bigcirc_B-algebras in complex vector spaces which are free on the tensor unit Vect\mathbb{C} \,\in\, \mathbb{C} Vect (the 1-dimensional complex vector space) play the role of (finite dimensional complex vector spaces underlying) Hilbert space of quantum states which are spanned by the set BB regarded as a “quantum measurement basis”.

For example, the dependent linear type of qbits is the free B\bigcirc_B-algebra Bool\bigcirc_{Bool} \mathbb{C} spanned by the classical type Bool ={0,1}= \{0,1\} of bits, reflecting the two canonical quantum measurement-outcomes (|0\vert 0\rangle, |1\vert 1 \rangle) of qbits.

Curiously, from this one finds that quantum measurement is exactly indefiniteness handling

where

  • “indefiniteness” is understood as the the effect/modality expressed by the reader monad B\bigcirc_B (see here),

  • “handling” is understood as effect handling in the sense of effect-monads in computer science (see here);

namely:

Notice that this process may be understood as the “dynamic lifting” of quantum measurement-results into the context (here: B=B = Bool) of the ambient dependent linear type theory.

For more on this see at quantum circuits via dependent linear types.


This naturally relates to the discussion of quantum measurement via Frobenius algebra-structures which is popular in the context of quantum information theory via dagger-compact categories – as follows:

Remark

(quantum reader monad is Frobenius)
Since the direct sum of vector spaces is a biproduct and using our running assumption that BB is a finite set, it follows that the underlying functor of the quantum reader monad from Prop. coincides with that of the coreader comonad, and hence that the quantum reader monad is a Frobenius monad (see there).

Remark

(quantum reader monad is special Frobenius writer monad)
Consider the BB-indexed the direct sum k Bk^{\otimes^B} of the ground field with itself as a kk-algebra and write

k B-Writer:VectVect {k^{\otimes^B}}\text{-}Writer \;\colon\; Vect \to Vect

for the writer monad corresponding to this monoid object in Vect: The monad which acts by forming the tensor product Writer k B(V)V(k B)Writer_{k^{\otimes^B}}(V) \;\coloneqq\; V \otimes \big( k^{\otimes^B} \big) and whose monad multiplication and unit of a monad are induced from the multiplication and unit in this monoid.

The above proof of Prop. shows at once that this writer monad is isomorphic to the BB-reader monad:

BWriter k B. \bigcirc_B \;\simeq\; Writer_{k^{\otimes^B}} \,.

Now the monad modules over a writer monad are just the ordinary modules over the corresponding monoid, so that

BMod(Vect)(k B)Mod(Vect). \bigcirc_B Mod(Vect) \;\simeq\; \big( k^{\otimes^B} \big)Mod(Vect) \,.

This provides a rather transparent re-derivation of and alternative perspective on Example .

Dually, as in Prop. , the quantum coreader comonad is isomorphic to the coreader comonad corresponding to the coalgebra-structure on k Bk^{\otimes^B}.

Hence, as a Frobenius monad (Prop. ), the quantum reader corresponds to k Bk^{\otimes^B} regarded as a Frobenius algebra, in fact as a commutative and special Frobenius algebra. In this form the quantum reader monad is prominent in the literature on quantum information theory via dagger-compact categories [Coecke & Pavlović (2008), §1.5.1, Coecke & Paquette (2008), §2.3].

(2)
(co)monad nameunderlying endofunctor(co)monad structure induced by
reader monadW(-)W \to (\text{-}) on cartesian typesunique comonoid structure on WW
coreader comonadW×(-)W \times (\text{-}) on cartesian typesunique comonoid structure on WW
writer monadA(-)A \otimes (\text{-}) on monoidal typeschosen monoid structure on AA
cowriter comonadA(-) A(-)\array{A \to (\text{-}) \\ \\ A \otimes (\text{-})} on monoidal typeschosen monoid structure on AA

chosen comonoid structure on AA
Frobenius (co)writerA(-) A(-)\array{A \to (\text{-}) \\ A \otimes (\text{-})} on monoidal typeschosen Frobenius monoid structure

References

General

As a monad in computer science:

See also:

A treatment of opacity in linguistics via the function monad

On linear types

The quantum reader monad – implicitly, in its incarnation as the k Bk^B-DualWriter monad – is highlighted in the literature quantum information theory via dagger-compact categories as formalizing “classical structures” (namely linear bases for quantum measurement):

The account above follows:

Last revised on August 11, 2023 at 11:28:36. See the history of this page for a list of all contributions to it.