Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created a minimum at function monad (aka “reader monad”, “environment monad”)
What can be said about algebras for the function/reader monad, $A \mapsto A^E$? I see Zhen Lin gives as an example a setting where for a function $p: I \to E$ and dependent $X(i)$, the product type $\prod_{i:I} X(i)$ is an algebra, where the action
$(\prod_{i:I} X(i))^E \to \prod_{i:I} X(i)$sends $f$ to $i \mapsto f(p(i))(i)$.
I guess you can think of that by factoring $\prod_{i: I} X(i)$ as $\prod_{e: E} \cdot \prod_p X(i)$?
Is there anything to be said more generally about these algebras?
It’s possible that $\prod_E: Set/E \to Set$ is monadic in general (the associated monad is this reader monad). I can check this at least in the case where $E$ is finite, using crude monadicity: $\prod_E$ preserves reflexive coequalizers since the latter are sifted colimits and these commute with finite products. It seems to be isomorphism-reflecting as well although a slick proof eludes me at the moment.
I’m not going to have any time during the remainder of today to look into the situation for more general $E$.
If I recall correctly, when $E=2$ then the algebras are precisely the rectangular bands.
Regarding #3, I don’t think $\prod_E$ reflects isos even for finite $E$. If I’m not mistaken, when $E=\{0,1\}$, then $\prod_E(X,k_0)=\prod_E(Y,k_0)=\emptyset$ for all $X$ and $Y$. Here $k_0$ is the constant $0$ function. Maybe I misunderstood #3.
Thanks, Sam. I see you’re talking about such things in Instances of computational effects:an algebraic perspective. I’d never heard of bands before. There’s then a ’rectangular bands monad’, as discussed here, which is $id \times id$ for the identity monad.
A whole new world!
Stupid me.
Thanks. It was also discussed at the cafe back in 2015 (here). Out of that came the observation that $\prod: NonEmptySet^2\to NonEmptySet$ is monadic. So perhaps, more generally, #3 can be rescued with some non-emptyness assumptions.
Have hyperlinked the term rectangular band, as per the discussion here.
In the section “Algebras for the reader monad” (here), where it said that these are hard to describe in general, I have added the remark that the reader monad makes sense in more general hyperdoctrines and that for dependent linear types the situation is different (due to/if one has existence of biproducts).
Then I added a section Examples – Quantum reader monad (here) which spells this out in some detail.
On this point, I guess the following is as trivial as it is noteworthy:
The “quantum reader monad”, i.e. the reader monad on $Vect$ which I had spelled out above (here), is evidently isomorphic to the writer monad (action monad) $(-) \otimes k^{\oplus_B}$, the one which tensors with the direct sum algebra consisting of $B$-indexed copies of the ground field. This naturally identifies the reader algebras with $\mathbb{C}^{\otimes_B}$-modules in the ordinary sense of modules over algebras.
Moreover, the underlying functor of the quantum reader coincides with that of the quantum co-reader, which translates to $k^{\oplus_B}$ also being a co-algebra – in fact a special symmetric Frobenius algebra. This way we may naturally identify linear (co)modules over the (co)reader (co)monads with ordinary (co)modules over this Frobenius algebra.
But this connects the discussion of quantum circuits via dependent linear types to the notion of “classical contexts” due to Coecke & Pavlović (2008).
Or rather, it will once one makes explicit the relevance of (co)modules in the latter approach, which pretty much happens in Heunen & Vicary (2019), say around Lem. 5.61 there.
( This is mostly a note to myself, I guess. Will flesh this out. )
I have polished up the diagram a little more (still here) and added a comment on the relation to “dynamic lifting”
I have added a diagram (here) summarizing the system of equivalences of the “quantum reader monad” over a finite base
and I have added explicit pointers to page and verse where Bob Coecke et al. mention (briefly) the monadic perspective on their “classical structures”:
Bob Coecke, Duško Pavlović, §1.5.1 of: Quantum measurements without sums, in Louis Kauffman, Samuel Lomonaco (eds.), Mathematics of Quantum Computation and Quantum Technology, Taylor & Francis (2008) 559-596 [arXiv:quant-ph/0608035, doi:10.1201/9781584889007]
Bob Coecke, Eric Oliver Paquette, §2.3 in: POVMs and Naimark’s theorem without sums, Electronic Notes in Theoretical Computer Science 210 (2008) 15-31 [arXiv:quant-ph/0608072, doi:10.1016/j.entcs.2008.04.015]
Bob Coecke, Eric Paquette, Dusko Pavlovic, Def. 2.8 in: Classical and quantum structures (2008) [pdf]
Next I am going to split this material off to a dedicated entry quantum reader monad.
I don’t understand well what are the unit and the multiplication of the reader monad in the introduction. Would it be possible to define them more explicitly?
Probably I’m a good example of a reader that doesn’t already know the subject before reading the entry and it lacks of details for such a reader in my opinion in the sense that I don’t understand the definition of the title.
Am on my phone, in a meeting. Will edit later, but just briefly:
The unit $D\to Maps(W,D)$ sends $d$ to the function on $W$ which has constant value $d$.
The multiplication $Maps(W, Maps(W,D)) \to Maps(W,D)$ sends $f(-)(-)$ to $w \mapsto f(w)(w)$.
Thanks, that’s already clearer with this.
Thanks, that’s excellent. I’m excited to see that you can define the reader monad in the generality of locally cartesian closed categories and so in a purely logical context if I understand. Is it difficult to prove that it is a monad in this generality?
The fact that $\bigcirc_B \coloneqq (p_B)_\ast (p_B)^\ast$ is a monad is immediate, since $(p_B)^\ast \dashv (p_B)_\ast$ is an adjoint pair (“right base change”). This means that the reader monad exists in much more generality than LCCCs even: I just needs a “right hyperdoctrine”.
E.g. the case of the “quantum reader monad” comes from the case of linear types dependent on classical types.
added pointer to:
1 to 26 of 26