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: coreader comonad

Bottom of Page

1 to 20 of 20

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeApr 18th 2015

    started a minimum at writer comonad

    • CommentRowNumber2.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 12th 2015
    • (edited Dec 18th 2019)

    So the writer comonad is a pull-push transform for the span *←W→*\ast \leftarrow W \rightarrow \ast.

    You said somewhere that reader and writer agree in certain contexts. Ah yes here. So there the randomness of the reader combines with the pull-pushnness of the writer, and we’re in the realm of path integrals.

    Does anything interesting happen in the relative case W 0←W→W 0W_0 \leftarrow W \rightarrow W_0? In modal terms this was supposed to be about a less than total accessibility relation on worlds. Does one ever pull-push through an equivalence relation?

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2015
    • (edited May 12th 2015)

    …and we’re in the realm of path integrals. Does anything interesting happen in the relative case W 0←W→W 0W_0 \leftarrow W \rightarrow W_0?

    This relative case is already what matters for the path integral here.

    In this context we are to think of the “possible worlds” more concretely as the “possible paths” or “possible trajectories” that a physical system may traverse. These are regarded here as depending on one of their two endpoints. “All possible histories w(w 0)∈W(w 0)w(w_0) \in W(w_0) starting at the world w 0∈W 0w_0 \in W_0.”

    • CommentRowNumber4.
    • CommentAuthorDavid_Corfield
    • CommentTimeMay 12th 2015

    Then the state monad passes through

    *←W→idW→*←W→*→*. \ast \leftarrow W \stackrel{id}{\rightarrow} W \rightarrow \ast \leftarrow W \rightarrow \ast \rightarrow \ast.

    What’s happening when reader and writer coincide? In that situation does it make sense to form a state monad which will just be reader (or writer) applied twice?

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeMay 12th 2015
    • (edited May 12th 2015)

    Yes, in that case it would just be the state monad applied twice.

    But it is here, I think, that switching from the terminology “reader”, “writer”, “state” to “randomness” becomes really compelling:

    on non-linear type then reader and writer will almost never coincide.

    On stable linear types however, there are interesting situations in which “reader” and “writer” coincide (namely if WW is “compact enough” such as to admit a Poincaré duality), but in this situation is interpretation in terms of “reading” and “writing” is maybe no longer the most immediate one (though in principle it still applies). The more immediate interpretation of what is going on in this case is that one is producing linear spaces of probability amplitudes.

    • CommentRowNumber6.
    • CommentAuthorDavid_Corfield
    • CommentTimeMar 13th 2021

    Reordered the Idea section.

    diff, v8, current

    • CommentRowNumber7.
    • CommentAuthorGuest
    • CommentTimeOct 28th 2022
    • (edited Oct 28th 2022 by Urs)

    [ This is me, Urs, speaking here – the system seems to have logged me out while I was compiling this comment. ]

    \,

    Here is a question on whether/how people think of the following from the logical perspective:

    When the writer B⊣reader Bwriter_B \dashv reader_B (co)monad pair is understood as coming from a hyperdoctrine or dependent type system, namely from the base change adjoint triple along BB, as:

    writer B≔∐B((−)×B)=(p B) !(p B) *−−−reader B≔∏B((−)×B)=(p B) *(p B) * writer_B \;\coloneqq\; \underset{B}{\coprod} \big((-)\times B\big ) \;=\; (p_B)_! (p_B)^\ast \phantom{---} reader_B \;\coloneqq\; \underset{B}{\prod} \big((-)\times B\big ) \;=\; (p_B)_\ast (p_B)^\ast

    then there is a real sense in which it is possible to “actually write/read a given element”:

    Namely, after pulling back (the value of) the reader monad to the context BB, there is a natural map

    (p B) *reader BH = (p B) *(p B) *(p B) *H →ε (p B) *H (p B) *H b:B⊢ ∏b′:BH →(h b′) b′:B↦h b H \array{ & (p_B)^\ast reader_B H &=& (p_B)^\ast (p_B)_\ast (p_B)^\ast H & \xrightarrow{ \;\;\; \epsilon_{ {}_{(p_B)^\ast H}} \;\;\; } & (p_B)^\ast H \\ {\color{purple}b} \colon B \;\; \vdash & && \underset{b' \colon B}{\prod} H & \xrightarrow{ (h_{b'})_{b' \colon B} \;\mapsto\; h_{\color{purple}b} } & H }

    which has the interpretation of:

    “Given an element b\color{purple}b of BB, read out the b\color{purple}bth component from the reader monad.”

    Dually, once we pull back the (value of the) writer comonad to the context, there is a natural map

    (p B) *H →η (p B) *H (p B) *(p B) !(p B) *H ≃ (p B) *writer BH b:B⊢ H →h↦(b,h) ∐b′:BH \array{ & (p_B)^\ast H &\xrightarrow{\; \eta_{{}_{(p_B)^\ast H}} \;}& (p_B)^\ast (p_B)_! (p_B)^\ast H &\simeq& (p_B)^\ast writer_B H \\ {\color{purple}b} \colon B \;\; \vdash & H & \xrightarrow{\; h \;\mapsto\; ( {\color{purple} b}, \, h) \;} & \underset{b' \colon B}{\coprod} H }

    which has the interpretation of:

    “Given an element b\color{purple}b of BB, write into the b\color{purple}bth component of the writer comonad.”

    \,

    One might say that what is happening here is that the parameter bb gets “lifted out of the type back into the context, where we may then again refer to it” – if you see what I mean.

    \,

    What I am wondering about is if anybody speaks/thinks about the reader/writer comonad in this way, as admitting a way to read/write “a definite value”, once we understand the situation as dependently typed.

    • CommentRowNumber8.
    • CommentAuthorGuest
    • CommentTimeOct 30th 2022
    The explanation about the computational interpretation of this comonad seems incorrect. The text discusses morphisms of the form X -> W x Y as intuitively encoding a computation that also writes a side-effect in Y. Although this sounds correct, the issue is we're talking about a comonad, so the form of a Kleisli map is W x Y -> Y. The computational interpretation then should be a computation that also reads from some fixed external environment W. (The naming Writer monad is then rather suspect in this regard, but does occur elsewhere. I believe environment or coReader comonad is also used). (Remark from Dan Marsden).
    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2022

    Yes, this is due to a mixup with the case where WW is equipped with monoid structure, where W×(−)W\times (-) is indeed a monad via that monoid structure, which then does model the idea of writing to a buffer.

    The entry should make that clear, and maybe terminology should be adjusted. I might have time for it later todsy.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2022

    I have now adjusted and slightly expanded the wording in the entry.

    Then I have dug out (or rather: took the best first two that I found) pointers to sources which say “reader comonad” or “coreader comonad”.

    (There is much room left to further expand, please feel invited to edit.)

    Finally I have renamed to “coreader comonad”.

    diff, v10, current

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2022
    • (edited Nov 1st 2022)

    also pointer to;

    diff, v11, current

    • CommentRowNumber12.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 8th 2022

    Added that this is also known as the product comonad and gave a reference to this.

    diff, v13, current

    • CommentRowNumber13.
    • CommentAuthormaxsnew
    • CommentTimeJun 3rd 2023

    Be a bit more precise about the conditions required for defining this comonad. Describe indexed comonad structure, add third name: environment comonad.

    diff, v15, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeJun 3rd 2023
    • (edited Jun 3rd 2023)

    fixed the link for exponentiable.

    (By default, nLab entry names are nouns. So we have an entry titled exponential object and exponentiable object is redirecting there. We could make the also the the adjective “exponentiable” redirect there if this is felt necessary.)

    diff, v16, current

    • CommentRowNumber15.
    • CommentAuthormaxsnew
    • CommentTimeJun 3rd 2023

    Coalgebras and the relationship to slice categories.

    diff, v17, current

    • CommentRowNumber16.
    • CommentAuthormaxsnew
    • CommentTimeJun 3rd 2023

    Fix a mistake in the statement about comonadicity of the slice category

    diff, v18, current

    • CommentRowNumber17.
    • CommentAuthorTodd_Trimble
    • CommentTimeJun 3rd 2023

    Corrected a typo, and took the liberty of giving the forgetful functor from the slice category a name.

    diff, v19, current

    • CommentRowNumber18.
    • CommentAuthormaxsnew
    • CommentTimeJun 4th 2023

    More specific link for coalgebra

    diff, v20, current

    • CommentRowNumber19.
    • CommentAuthormaxsnew
    • CommentTimeJun 8th 2023

    Describe the generalization to tensor products.

    diff, v21, current

    • CommentRowNumber20.
    • CommentAuthorncfavier
    • CommentTimeFeb 6th 2024

    Mentioned the duality with exception monads.

    diff, v24, current

1 to 20 of 20

  1.