Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: function monad

Bottom of Page

1 to 27 of 27

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeApr 17th 2015
    • (edited Apr 17th 2015)

    created a minimum at function monad (aka “reader monad”, “environment monad”)

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2018
    • (edited Dec 9th 2018)

    What can be said about algebras for the function/reader monad, A↦A EA \mapsto A^E? I see Zhen Lin gives as an example a setting where for a function p:I→Ep: I \to E and dependent X(i)X(i), the product type ∏ i:IX(i)\prod_{i:I} X(i) is an algebra, where the action

    (∏ i:IX(i)) E→∏ i:IX(i) (\prod_{i:I} X(i))^E \to \prod_{i:I} X(i)

    sends ff to i↦f(p(i))(i)i \mapsto f(p(i))(i).

    I guess you can think of that by factoring ∏ i:IX(i)\prod_{i: I} X(i) as ∏ e:E⋅∏ pX(i)\prod_{e: E} \cdot \prod_p X(i)?

    Is there anything to be said more generally about these algebras?

    • CommentRowNumber3.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 9th 2018

    It’s possible that ∏ E:Set/E→Set\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 EE is finite, using crude monadicity: ∏ E\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 EE.

    • CommentRowNumber4.
    • CommentAuthorSam Staton
    • CommentTimeDec 9th 2018
    • (edited Dec 9th 2018)

    If I recall correctly, when E=2E=2 then the algebras are precisely the rectangular bands.

    Regarding #3, I don’t think ∏ E\prod_E reflects isos even for finite EE. If I’m not mistaken, when E={0,1}E=\{0,1\}, then ∏ E(X,k 0)=∏ E(Y,k 0)=∅\prod_E(X,k_0)=\prod_E(Y,k_0)=\emptyset for all XX and YY. Here k 0k_0 is the constant 00 function. Maybe I misunderstood #3.

    • CommentRowNumber5.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2018
    • (edited Dec 9th 2018)

    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×idid \times id for the identity monad.

    A whole new world!

    • CommentRowNumber6.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 9th 2018

    Stupid me.

    • CommentRowNumber7.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 9th 2018

    I’ve added something on algebras.

    diff, v14, current

    • CommentRowNumber8.
    • CommentAuthorSam Staton
    • CommentTimeDec 9th 2018

    Thanks. It was also discussed at the cafe back in 2015 (here). Out of that came the observation that ∏:NonEmptySet 2→NonEmptySet\prod: NonEmptySet^2\to NonEmptySet is monadic. So perhaps, more generally, #3 can be rescued with some non-emptyness assumptions.

  9. Link to “Monads as a solution for Generalised Opacity” paper was no longer live. Found another place it is published

    henry.story@bblfish.net

    diff, v15, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeJan 8th 2021
    • (edited Jan 8th 2021)

    Have hyperlinked the term rectangular band, as per the discussion here.

    diff, v17, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2022

    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.

    diff, v19, current

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022

    Added an example/remark (here) with comments on the case of free quantum reader algebras.

    diff, v22, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2022
    • (edited Nov 6th 2022)

    On this point, I guess the following is as trivial as it is noteworthy:

    The “quantum reader monad”, i.e. the reader monad on VectVect which I had spelled out above (here), is evidently isomorphic to the writer monad (action monad) (−)⊗k ⊕ B(-) \otimes k^{\oplus_B}, the one which tensors with the direct sum algebra consisting of BB-indexed copies of the ground field. This naturally identifies the reader algebras with ℂ ⊗ B\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 ⊕ Bk^{\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. )

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeNov 7th 2022

    I have added remarks on how the quantum reader monad (for finite indexed set) is (1.) Frobenius (here) and (2.) isomorphic to the writer monad induced by a special symmetric Frobenius algebra (here).

    diff, v23, current

    • CommentRowNumber15.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2022

    I have added a brief paragraph (here) on the Kleisli category of the reader monad on set

    diff, v25, current

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeNov 8th 2022

    I have added (here) a diagram which shows how “effect handling” for the quantum reader monad expresses quantum measurement.

    diff, v26, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeNov 9th 2022

    I have polished up the diagram a little more (still here) and added a comment on the relation to “dynamic lifting”

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2022
    • (edited Nov 12th 2022)

    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”:

    Next I am going to split this material off to a dedicated entry quantum reader monad.

    diff, v29, current

    • CommentRowNumber19.
    • CommentAuthorJ-B Vienney
    • CommentTimeNov 25th 2022
    • (edited Nov 25th 2022)

    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.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2022

    Am on my phone, in a meeting. Will edit later, but just briefly:

    The unit D→Maps(W,D)D\to Maps(W,D) sends dd to the function on WW which has constant value dd.

    The multiplication Maps(W,Maps(W,D))→Maps(W,D)Maps(W, Maps(W,D)) \to Maps(W,D) sends f(−)(−)f(-)(-) to w↦f(w)(w) w \mapsto f(w)(w).

    • CommentRowNumber21.
    • CommentAuthorJ-B Vienney
    • CommentTimeNov 25th 2022

    Thanks, that’s already clearer with this.

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2022
    • (edited Nov 25th 2022)

    Okay, I have typed up a Definition-section (here).

    The formulas are fairly detailed and complete, while the text around them leaves rooom to be polished up further. But I am out of steam for this now and will leave it as is for the moment.

    diff, v31, current

    • CommentRowNumber23.
    • CommentAuthorJ-B Vienney
    • CommentTimeNov 25th 2022
    • (edited Nov 25th 2022)

    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?

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeNov 25th 2022
    • (edited Nov 25th 2022)

    The fact that ◯ B≔(p B) *(p B) *\bigcirc_B \coloneqq (p_B)_\ast (p_B)^\ast is a monad is immediate, since (p B) *⊣(p B) * (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.

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeNov 26th 2022
    • (edited Nov 26th 2022)

    I have tried to combine into one single place (now here) what ended up being a multitude of scattered allusions on relation of the reader monad to the state monad – and then I tried to stream-line the result.

    Still much room left, though, to polish this all up..

    diff, v33, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeAug 10th 2023

    added pointer to:

    diff, v38, current

    • CommentRowNumber27.
    • CommentAuthorvarkor
    • CommentTimeSep 21st 2024

    Corrected a misleading assertion.

    diff, v40, current

1 to 27 of 27

  1.