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

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 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 homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft 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).

nLab > Latest Changes: monad (in computer science)

Bottom of Page

1 to 46 of 46

  1.  
    • 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

  11. 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◯ B∐B′:FinType◯ B′≃∐B:FinType∐B′:FinType◯ B◯ B′≃∐B,B′:FinType◯ B×B′⟶∐B″: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,B′B, B' on the left identically onto the summand indexed by B″=B×B′B'' = 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.

    • CommentRowNumber24.
    • CommentAuthorUrs
    • CommentTimeMar 15th 2023

    added pointer to:

    diff, v92, current

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeAug 8th 2023
    • (edited Aug 8th 2023)

    added pointer to:

    diff, v94, current

    • CommentRowNumber26.
    • CommentAuthorUrs
    • CommentTimeAug 14th 2023
    • (edited Aug 14th 2023)

    have added (here) a slide from Overton 2014 tabulating (co)monad-terminology in Haskell

    diff, v98, current

    • CommentRowNumber27.
    • CommentAuthorUrs
    • CommentTimeAug 15th 2023

    finally added to the subsection on dual comonadic contexts (here, scroll down to the end of the subsection) the dual diagram to the very first one in the entry

    diff, v99, current

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeAug 22nd 2023

    only now discovered this review:

    diff, v101, current

    • CommentRowNumber29.
    • CommentAuthorUrs
    • CommentTimeAug 26th 2023

    I am going to add a section explaining “do notation”.

    Just a question on referencing:

    Is there any canonical/citable systematic account of do-notation, such as in a textbook?

    I see many webpages and online tutorials on the matter (all of them opt for explanation-by-example). The closest to a textbook account that I am aware of is Milewski 2019, Sec. 20.3.

    (NB.: I am not asking for an explanation of the matter, but about how to cite and attribute it.)

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeAug 26th 2023
    • (edited Aug 26th 2023)

    Started a pagraph on do-notation (here)

    (also found the original references, from HHPW07, p. 25)

    diff, v105, current

    • CommentRowNumber31.
    • CommentAuthorRodMcGuire
    • CommentTimeAug 26th 2023

    all of them opt for explanation-by-example

    “do notation” is just a clever syntactic sugar hack and it was introduced by example.

    It showed up in Haskell 1.3 (May 1996) which added monadic IO and do-notation.

    https://www.haskell.org/definition/from12to13.html#do.

    A history of Haskell: being lazy with class (2007)

    https://doi.org/10.1145/1238844.1238856

    says the sugar was invented in 1994 by Mark Jones.

    Moving to take a post-doctoral post at Yale in 1992, [Mark] Jones continued to develop and maintain Gofer, adding support for constructor classes (Section 6.4) in 1992–93 and producing the first implementation of the do-notation in 1994

    • CommentRowNumber32.
    • CommentAuthorUrs
    • CommentTimeAug 26th 2023

    Thanks! – but we overlapped here. I had just found these references and added them above.

    I do think there is room to explain this stuff better. But I understand that in the community it is being picked up by osmosis.

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeAug 27th 2023

    have now expanded the section on Do-notation (here)

    diff, v107, current

    • CommentRowNumber34.
    • CommentAuthorRodMcGuire
    • CommentTimeAug 27th 2023

    off topic but maybe related. The article currently says:

    in general it may be misleading to think of Kleisli composition as being about “reading out” data. What Kleisli composition is really about is acting on data that has generators and defining a program by what it does on generators, hence for a given generator.

    In a category of presheaves Set C opSet^{C^op}, morphisms between presheaves have to agree on all of the morphisms of CC. However if CC has a simple presentation as generators and possibly relations one only has to check presheaf morphisms for agreement on the generator morphisms - if they agree then automatically so do the generated ones. e.g. If M1M1 is the free monoid on one generator ss then morphisms in Set M1 opSet^{M1^op} will agree on ss and one can safely ignore s 2s^2, s 3s^3, … as clutter.

    Even though this suppression often appears in pictures I can’t find it explicitly stated in the nLab.

    • CommentRowNumber35.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 27th 2023

    Rod, I don’t follow. CC is any category I guess. What do you mean by “morphisms between presheaves have to agree on all of the morphisms of CC”. The only meaning I can think of for a value of a morphism ϕ\phi between presheaves on CC at a morphism ff of CC is the diagonal of a naturality square formed from the data ϕ,f\phi, f. But two morphisms ϕ,ψ\phi, \psi of presheaves don’t have to agree (in this sense of value) at a morphism ff. You must be trying to say something else.

    • CommentRowNumber36.
    • CommentAuthorRodMcGuire
    • CommentTimeAug 27th 2023
    • (edited Aug 28th 2023)

    You must be trying to say something else.

    I was trying to concisely express things from a category of elements perspective. The category of elements of a presheaf can be regarded as a category with its objects and morphisms labeled by the objects and morphisms of CC. A morphism of presheafs on CC must agree on these labels - it can’t map a s 2s^2 element morphism to a s 1s^1 one.

    • CommentRowNumber37.
    • CommentAuthorTodd_Trimble
    • CommentTimeAug 28th 2023

    Much clearer. You are referring to the functor el:Set C→Cat/Cel: Set^C \to Cat/C, where natural transformations ϕ:F→G\phi: F \to G induce functors fitting in commutative squares

    el(F) →el(ϕ) el(G) ↓ ↓ C →1 C C\array{ el(F) & \stackrel{el(\phi)}{\to} & el(G) \\ \downarrow & & \downarrow \\ C & \stackrel{1_C}{\to} & C}

    where the “agreement” in #34 implicitly refers el(F)el(F) lying over the identity functor at the bottom. I believe el:Set C→Cat/Cel: Set^C \to Cat/C is full and faithful, although the article category of elements doesn’t seem to say that. Maybe you meant to suggest that as well: the criterion for when a functor el(F)→el(G)el(F) \to el(G) “is” a presheaf morphism F→GF \to G is this lying over CC, and maybe you are suggesting a further strengthening of this criterion in terms of generating morphisms.

    • CommentRowNumber38.
    • CommentAuthorUrs
    • CommentTimeAug 28th 2023

    The question in #34 is about functors (presheaves) on a free category over a graph 𝒢\mathcal{G}, observing that morphisms between them (natural transformations) are fixed as soon as they are fixed on the underlying graph.

    This is just the free category adjunction F:Grph→CatF \colon Grph \to Cat applied to natural transformations understood as functors out of the product with the interval category II:

    Mor(Func(F(𝒢),Set))=Hom Cat(F(𝒢)×I,Set)=Hom Cat(F(𝒢),Func(I,Set))=Hom Grph(𝒢,Func(I,Set)). Mor\Big( Func\big( F(\mathcal{G}) ,\, Set \big) \Big) \;\;=\;\; Hom_{Cat}\Big( F(\mathcal{G}) \times I ,\, Set \Big) \;\;=\;\; Hom_{Cat}\Big( F(\mathcal{G}) ,\, Func(I, Set) \Big) \;\;=\;\; Hom_{Grph}\Big( \mathcal{G} ,\, Func(I, Set) \Big) \,.

    \,

    Now, this question was apparently prompted by me highlighting (here, in a context of discussing appropriate programming syntax for them) that Kleisli morphisms are to be understood as operating on generators — which is of course just the same kind of free/forgetful phenomenon, now in the case of free modules over a given monad.

    There is a lot of interesting material in the entry of this thread (which is monads in computer science), that would be fun to discuss.

    Further discussion of maps of presheaves should be taken elsewhere. You could take this to the thread category of presheaves or, if really needed, category of elements.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeSep 10th 2023

    added pointer to:

    diff, v116, current

    • CommentRowNumber40.
    • CommentAuthorUrs
    • CommentTimeSep 15th 2023

    added what seem to be original references on effect handling via monad modules:

    diff, v120, current

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeSep 16th 2023

    added pointer to:

    • Eugenio Moggi, An abstract View of Programming Languages, LFCS report ECS-LFCS-90-113 [web, pdf]

    (which considers also monad transformations, Def. 4.0.8)

    diff, v121, current

    • CommentRowNumber42.
    • CommentAuthorUrs
    • CommentTimeSep 16th 2023

    added pointer to:

    diff, v122, current

    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeSep 17th 2023
    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeSep 27th 2023

    have improved the first slides-like graphics on bind/return operations (here)

    diff, v124, current

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeOct 26th 2023

    am taking the liberty of adding pointer to:

    diff, v129, current

  46. updated link to Martin Hyland preprint

    Anonymouse

    diff, v132, current

1 to 46 of 46

  1.