Not signed in (Sign In)

Start a new discussion

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

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor galois-theory gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homology homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory itex k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes science set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeOct 29th 2022

    added pointer to:

    • Rob Norris, Functional Programming with Effects, talk at Scala Days 2018 [video: YT]

    diff, v56, current

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2022
    • (edited Oct 31st 2022)

    I like to add to the entry monad in computer science a more useful Idea-section.

    A first version of the kind of exposition that I have in mind is now in the Sandbox – comments are welcome.

    I’ll try to polish this up a little more, but it seems I will keep being interrupted a lot today.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2022

    added pointer to:

    • Christina Kohl, Christina Schwaiger, Monads in Computer Science (2021) [pdf]

    diff, v59, current

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeOct 31st 2022
    • (edited Oct 31st 2022)

    added pointer to:

    diff, v59, current

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2022

    added these pointers:

    • Tarmo Uustalu, lecure notes for MGS 2021 (2021):

      Monads and Interaction Lecture 1 [pdf]

      Monads and Interaction Lecture 2 [pdf]

      Monads and Interaction Lecture 3 [pdf]

      Monads and Interaction Lecture 4 [pdf]

    diff, v61, current

    • CommentRowNumber6.
    • CommentAuthorUrs
    • CommentTimeNov 1st 2022

    have added pointer to

    for substantiation of what in the entry so far remains just a vague comment.

    diff, v62, current

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeNov 2nd 2022
    • (edited Nov 2nd 2022)

    Okay, I have now put in a new Idea-section.

    1. It starts (here) with a slightly polished adjustment of the previous idea-paragraph, which is (and was) really too short to serve as an actual exposition, but which may serve the purpose of quickly showing the impatient reader much of the relevant terminology.

    2. The main addition is a new sub-section Basic Idea: External monads (here) which means to be more like an actual exposition to a reader who does not already know.

      (This is a little longer than the terse paragraph that we had before, but meant to still be right to the point. I find most introductions in the literature are too long-winded and too mysterious-sounding. My motivation in writing this new subsection was to improve on this. You judge if it worked.)

    3. After this there is now one more subsection Refined idea: enriched monads (here), which means to admit to the technical subtleties while keeping them out of the way of the previous conceptual explanation.

      Compared to the rather mysterious-sounding side-remark that we had on this point before, this sub-section should be an improvement already, but I have not been ambitious about this subsection and don’t regard it as finished. But I’ll leave it as is for the time being.

    Next, the Examples-section really deserves to be polished up. But I haven’t looked into that yet.

    [edit: Have begun to bring at least some structure into the Exaples-section ]

    diff, v66, current

    • CommentRowNumber8.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2022

    added prominent pointer to extension system that had been missing all along

    diff, v72, current

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2022

    I have prefixed the list of references (here) with pointer to extension systems:

    diff, v73, current

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2022

    I have started an analogous Idea-subsection on algebras/modules (here) and began some sketch on the comonad version of it all (here).

    In the course of this I changed the notation for the monad from “TT” to “\mathcal{E}”, throughout (for “Effect”) so that I can use “𝒞\mathcal{C}” for the comonads (“Cause”!?)

    But I am running out of steam now, and, more importantly, I need to be looking into preparing slides for a talk I give tomorrow, on a completely different subject.

    diff, v76, current

  1. I wonder what the computer science interpretation (in terms of cause and effect on programs) of the cohesive modalities are. Sharp and shape are both monadic, while flat is comonadic.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeNov 3rd 2022
    • (edited Nov 3rd 2022)

    I believe that for idempotent monads one may think of their effect as that of forgetting or “making invisible” some aspects of the data, or more precisely as projecting out a certain sub-aspect of the data (and in that way, their presence witnesses that the computer system potentially has a richer data structure than usual, so that it is possible to forget some of it, in the first place).

    So if a program produces ʃDD-data, then that can be thought of as DD-data but with the extra effect that it becomes impossible to see some aspects usually carried by DD-data (namely the cohesive aspect).

    Similarly, a program reading in D\flat D-data needs, to run, an agent that strips some cohesive qualities off of full DD-data.

    I guess one can see the effect-picture of the “axiomatic” modalites rather vividly from the fact that existing proof assistants do not implement them: Much like IO in Haskell, they are (or will be) an extra feature (effect) that needs to be provided by the ambient computer system.

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

    I have now added a graphics showing all the monad algebra structure and properties in extension/Kleisli form (see here and scroll down a little).

    In doing do, I realized that my square-bracket notion for binding, clever as it seemed in itself, is not sustainable as more such operations come into consideration, and so I have rewritten the whole entry (I hope, let me know if you spot remaining glitches) using

    • bind bind^{\mathcal{E}} for “binding”

    • ret ret^{\mathcal{E}} for “returning”

    and now

    • hndl hndl^{\mathcal{E}} for “handling” (i.e. for the monad action morphism).

    This way there is now also room for the comonadfc versions

    • extr extr^{\mathcal{E}} for “exracting” (the counit)

    etc., and then something like

    • caus caus^{\mathcal{E}} for “causing”

    or maybe

    • prod prod^{\mathcal{E}} for “producing”

    for a comonad co-action. Still undecided which term to best use (and the literature seems not to offer suggestions on this point?)

    diff, v79, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeNov 6th 2022

    added a paragraph (here) on the free \mathcal{E}-effect handlers and how they formalize the motivating intuition at the beginning of the entry, that “binding” means to handle \mathcal{E}-effects by “carrying them along”.

    diff, v82, current

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 6th 2022

    Added

    • The selection monad encodes selecting a value of a type depending on the values taken by some function on it.

    Perhaps there’s a better way to describe what it does.

    diff, v83, current

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeNov 9th 2022

    added this pointer:

    Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, Flavien Breuvart, Tarmo Uustalu, Combining effects and coeffects via grading, ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (2016) 476–489 [doi:10.1145/2951913.2951939, talk abstract, video rec]

    diff, v86, current

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2022
    • (edited Nov 14th 2022)

    Just a trivial question on how people speak:

    What is the terminology, in programming practice, for the dual of monadic effect handling?

    I.e. given a comonadic co-effect on a data type system, what is the terminology for the co-action on co-algebras?

    I gather the comonadic co-effect itself is addressed as providing “context”. Now a co-effect co-handler could reasonably be said to “produce” or “provide” such a context.

    For instance, it seems to make perfect and immediate sense to say that a co-algebra for the co-reader co-monad is a routine/method that “provides a global parameter value”.

    But does anyone speak this way, in the actual (functional) programming practice? Or is there other common terminology for this purpose?

    Or is there maybe not much of an established tradition of talking about comonadic co-effect co-handlers at all?

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2022

    added pointer to

    diff, v87, current

    • CommentRowNumber19.
    • CommentAuthorUrs
    • CommentTimeNov 14th 2022

    re #17:

    Uustalu on slide 9 of part 3 of his 2021 lecture (as linked to in the entry, can’t easily hyperlink from my phone here) says:

    coeffect producer (should we call it a cohandler?)

    So with “co-effect” = “context” this is the first of my two suggestions in #17: “context producer”.

    Hm, somehow I’d like “context provider” better…

    diff, v89, current

    • CommentRowNumber20.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 14th 2022

    Some thoughts over here. Apparently, they speak of ’capabilities’ being provided.

    • CommentRowNumber21.
    • CommentAuthorDavid_Corfield
    • CommentTimeNov 14th 2022

    It seems that

    • Jack B. Dennis, Earl C. Van Horn, Programming semantics for multiprogrammed computations, Communications of the ACM Volume 9 Issue 3 March 1966 pp 143–155 doi:10.1145/365230.365252

    introduces this idea of ’capability’.

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

    Thanks!

    I have now glanced over the provided references using the word “capabilities”, but so far I have trouble seeing that these are really referring to coalgebras over comonads. Maybe I find time to have a closer loock.

    But I did find Petricek et al’s articles using “contexts” for “coeffects” and they are clear enough. While this is not what I asked (and the interpretation of comonads as “contexts” is already in Uustalu & Vene), I am adding this pointer to the entry now, for completeness:

    • Tomas Petricek, Dominic Orchard, Alan Mycroft, Coeffects: Unified Static Analysis of Context-Dependence, in: Automata, Languages, and Programming. ICALP 2013, Lecture Notes in Computer Science 7966 Springer (2013) [doi:10.1007/978-3-642-39212-2_35]

    diff, v90, current

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeDec 12th 2022
    • (edited Dec 12th 2022)

    This is a question on whether the following monad has been considered – as a tool in stochastic programming.

    I am considering the following in a context of quantum programming, but the general principle should be more general and I’d be happy to hear that people have considered classical variants.

    Namely, to model repeat-until-success algorithms, we need a way to “discard” (forget, ignore, disregard) quantum measurement results (modeled by the quantum reader monad B\bigcirc_B) without however dropping the quantum state that we are in after the measurement.

    For this purpose consider the functor on linear types \mathcal{H} that assigns

    B:FinType B \mathcal{H} \;\; \mapsto \;\; \underset{ B \colon FinType }{\coprod} \bigcirc_B \mathcal{H}

    which boils down to forming one big direct sum

    =B:FinType B. \cdots \;=\; \underset{ B \colon FinType }{\bigoplus} \oplus_B \mathcal{H} \,.

    This construction should become a monad with multiplication given by

    B:FinType BB:FinType BB:FinTypeB:FinType B BB,B:FinType B×BB:FinType B \underset{B \colon FinType}{\coprod} \,\bigcirc_B\, \underset{B' \colon FinType}{\coprod} \,\bigcirc_{B'}\, \;\simeq\; \underset{B \colon FinType}{\coprod} \underset{B' \colon FinType}{\coprod} \,\bigcirc_B\, \,\bigcirc_{B'}\, \;\simeq\; \underset{B, B' \colon FinType}{\coprod} \,\bigcirc_{B \times B'}\, \;\longrightarrow\; \underset{B'' \colon FinType}{\coprod} \,\bigcirc_{B''}\,

    where the last step maps any summand indexed by B,BB, B' on the left identically onto the summand indexed by B=B×BB'' = B \times B' on the right.

    This monad comes with natural transformations to “absorb” instances of B\bigcirc_B in the evident sense. Repeat-until-success algorithms are recursive functions with values in this monad which on a given input produce the infinite tree of all possible sequences of syndrome=fail measurements followed by a last syndrome=success measurement, each parameterizing the corresponding quantum state after that number of measurements.

    (If you see what I mean. I am in the process of typing this up and can try to show more details on what I am after, later.)

    I have played with other variants before arriving at the above formula, simple as it all is. But I still feel like I may be missing a more profound underlying principle that I should be invoking here.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)