CINXE.COM
monad (in computer science) in nLab
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1 plus MathML 2.0 plus SVG 1.1//EN" "http://www.w3.org/2002/04/xhtml-math-svg/xhtml-math-svg-flat.dtd" > <html xmlns="http://www.w3.org/1999/xhtml"> <head> <title> monad (in computer science) in nLab </title> <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /> <meta name="robots" content="index,follow" /> <meta name="viewport" content="width=device-width, initial-scale=1" /> <link href="/stylesheets/instiki.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/mathematics.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/syntax.css?1660229990" media="all" rel="stylesheet" type="text/css" /> <link href="/stylesheets/nlab.css?1676280126" media="all" rel="stylesheet" type="text/css" /> <link rel="stylesheet" type="text/css" href="https://cdn.jsdelivr.net/gh/dreampulse/computer-modern-web-font@master/fonts.css"/> <style type="text/css"> h1#pageName, div.info, .newWikiWord a, a.existingWikiWord, .newWikiWord a:hover, [actiontype="toggle"]:hover, #TextileHelp h3 { color: #226622; } a:visited.existingWikiWord { color: #164416; } </style> <style type="text/css"><!--/*--><![CDATA[/*><!--*/ .toc ul {margin: 0; padding: 0;} .toc ul ul {margin: 0; padding: 0 0 0 10px;} .toc li > p {margin: 0} .toc ul li {list-style-type: none; position: relative;} .toc div {border-top:1px dotted #ccc;} .rightHandSide h2 {font-size: 1.5em;color:#008B26} table.plaintable { border-collapse:collapse; margin-left:30px; border:0; } .plaintable td {border:1px solid #000; padding: 3px;} .plaintable th {padding: 3px;} .plaintable caption { font-weight: bold; font-size:1.1em; text-align:center; margin-left:30px; } /* Query boxes for questioning and answering mechanism */ div.query{ background: #f6fff3; border: solid #ce9; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; max-height: 20em; overflow: auto; } /* Standout boxes for putting important text */ div.standout{ background: #fff1f1; border: solid black; border-width: 2px 1px; padding: 0 1em; margin: 0 1em; overflow: auto; } /* Icon for links to n-category arXiv documents (commented out for now i.e. disabled) a[href*="http://arxiv.org/"] { background-image: url(../files/arXiv_icon.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 22px; } */ /* Icon for links to n-category cafe posts (disabled) a[href*="http://golem.ph.utexas.edu/category"] { background-image: url(../files/n-cafe_5.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pdf files (disabled) a[href$=".pdf"] { background-image: url(../files/pdficon_small.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ /* Icon for links to pages, etc. -inside- pdf files (disabled) a[href*=".pdf#"] { background-image: url(../files/pdf_entry.gif); background-repeat: no-repeat; background-position: right bottom; padding-right: 25px; } */ a.existingWikiWord { color: #226622; } a.existingWikiWord:visited { color: #226622; } a.existingWikiWord[title] { border: 0px; color: #aa0505; text-decoration: none; } a.existingWikiWord[title]:visited { border: 0px; color: #551111; text-decoration: none; } a[href^="http://"] { border: 0px; color: #003399; } a[href^="http://"]:visited { border: 0px; color: #330066; } a[href^="https://"] { border: 0px; color: #003399; } a[href^="https://"]:visited { border: 0px; color: #330066; } div.dropDown .hide { display: none; } div.dropDown:hover .hide { display:block; } div.clickDown .hide { display: none; } div.clickDown:focus { outline:none; } div.clickDown:focus .hide, div.clickDown:hover .hide { display: block; } div.clickDown .clickToReveal, div.clickDown:focus .clickToHide { display:block; } div.clickDown:focus .clickToReveal, div.clickDown .clickToHide { display:none; } div.clickDown .clickToReveal:after { content: "A(Hover to reveal, click to "hold")"; font-size: 60%; } div.clickDown .clickToHide:after { content: "A(Click to hide)"; font-size: 60%; } div.clickDown .clickToHide, div.clickDown .clickToReveal { white-space: pre-wrap; } .un_theorem, .num_theorem, .un_lemma, .num_lemma, .un_prop, .num_prop, .un_cor, .num_cor, .un_defn, .num_defn, .un_example, .num_example, .un_note, .num_note, .un_remark, .num_remark { margin-left: 1em; } span.theorem_label { margin-left: -1em; } .proof span.theorem_label { margin-left: 0em; } :target { background-color: #BBBBBB; border-radius: 5pt; } /*]]>*/--></style> <script src="/javascripts/prototype.js?1660229990" type="text/javascript"></script> <script src="/javascripts/effects.js?1660229990" type="text/javascript"></script> <script src="/javascripts/dragdrop.js?1660229990" type="text/javascript"></script> <script src="/javascripts/controls.js?1660229990" type="text/javascript"></script> <script src="/javascripts/application.js?1660229990" type="text/javascript"></script> <script src="/javascripts/page_helper.js?1660229990" type="text/javascript"></script> <script src="/javascripts/thm_numbering.js?1660229990" type="text/javascript"></script> <script type="text/x-mathjax-config"> <!--//--><![CDATA[//><!-- MathJax.Ajax.config.path["Contrib"] = "/MathJax"; MathJax.Hub.Config({ MathML: { useMathMLspacing: true }, "HTML-CSS": { scale: 90, extensions: ["handle-floats.js"] } }); MathJax.Hub.Queue( function () { var fos = document.getElementsByTagName('foreignObject'); for (var i = 0; i < fos.length; i++) { MathJax.Hub.Typeset(fos[i]); } }); //--><!]]> </script> <script type="text/javascript"> <!--//--><![CDATA[//><!-- window.addEventListener("DOMContentLoaded", function () { var div = document.createElement('div'); var math = document.createElementNS('http://www.w3.org/1998/Math/MathML', 'math'); document.body.appendChild(div); div.appendChild(math); // Test for MathML support comparable to WebKit version https://trac.webkit.org/changeset/203640 or higher. div.setAttribute('style', 'font-style: italic'); var mathml_unsupported = !(window.getComputedStyle(div.firstChild).getPropertyValue('font-style') === 'normal'); div.parentNode.removeChild(div); if (mathml_unsupported) { // MathML does not seem to be supported... var s = document.createElement('script'); s.src = "https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.7/MathJax.js?config=MML_HTMLorMML-full"; document.querySelector('head').appendChild(s); } else { document.head.insertAdjacentHTML("beforeend", '<style>svg[viewBox] {max-width: 100%}</style>'); } }); //--><!]]> </script> <link href="https://ncatlab.org/nlab/atom_with_headlines" rel="alternate" title="Atom with headlines" type="application/atom+xml" /> <link href="https://ncatlab.org/nlab/atom_with_content" rel="alternate" title="Atom with full content" type="application/atom+xml" /> <script type="text/javascript"> document.observe("dom:loaded", function() { generateThmNumbers(); }); </script> </head> <body> <div id="Container"> <div id="Content"> <h1 id="pageName"> <span style="float: left; margin: 0.5em 0.25em -0.25em 0"> <svg xmlns="http://www.w3.org/2000/svg" width="1.872em" height="1.8em" viewBox="0 0 190 181"> <path fill="#226622" d="M72.8 145c-1.6 17.3-15.7 10-23.6 20.2-5.6 7.3 4.8 15 11.4 15 11.5-.2 19-13.4 26.4-20.3 3.3-3 8.2-4 11.2-7.2a14 14 0 0 0 2.9-11.1c-1.4-9.6-12.4-18.6-16.9-27.2-5-9.6-10.7-27.4-24.1-27.7-17.4-.3-.4 26 4.7 30.7 2.4 2.3 5.4 4.1 7.3 6.9 1.6 2.3 2.1 5.8-1 7.2-5.9 2.6-12.4-6.3-15.5-10-8.8-10.6-15.5-23-26.2-31.8-5.2-4.3-11.8-8-18-3.7-7.3 4.9-4.2 12.9.2 18.5a81 81 0 0 0 30.7 23c3.3 1.5 12.8 5.6 10 10.7-2.5 5.2-11.7 3-15.6 1.1-8.4-3.8-24.3-21.3-34.4-13.7-3.5 2.6-2.3 7.6-1.2 11.1 2.8 9 12.2 17.2 20.9 20.5 17.3 6.7 34.3-8 50.8-12.1z"/> <path fill="#a41e32" d="M145.9 121.3c-.2-7.5 0-19.6-4.5-26-5.4-7.5-12.9-1-14.1 5.8-1.4 7.8 2.7 14.1 4.8 21.3 3.4 12 5.8 29-.8 40.1-3.6-6.7-5.2-13-7-20.4-2.1-8.2-12.8-13.2-15.1-1.9-2 9.7 9 21.2 12 30.1 1.2 4 2 8.8 6.4 10.3 6.9 2.3 13.3-4.7 17.7-8.8 12.2-11.5 36.6-20.7 43.4-36.4 6.7-15.7-13.7-14-21.3-7.2-9.1 8-11.9 20.5-23.6 25.1 7.5-23.7 31.8-37.6 38.4-61.4 2-7.3-.8-29.6-13-19.8-14.5 11.6-6.6 37.6-23.3 49.2z"/> <path fill="#193c78" d="M86.3 47.5c0-13-10.2-27.6-5.8-40.4 2.8-8.4 14.1-10.1 17-1 3.8 11.6-.3 26.3-1.8 38 11.7-.7 10.5-16 14.8-24.3 2.1-4.2 5.7-9.1 11-6.7 6 2.7 7.4 9.2 6.6 15.1-2.2 14-12.2 18.8-22.4 27-3.4 2.7-8 6.6-5.9 11.6 2 4.4 7 4.5 10.7 2.8 7.4-3.3 13.4-16.5 21.7-16 14.6.7 12 21.9.9 26.2-5 1.9-10.2 2.3-15.2 3.9-5.8 1.8-9.4 8.7-15.7 8.9-6.1.1-9-6.9-14.3-9-14.4-6-33.3-2-44.7-14.7-3.7-4.2-9.6-12-4.9-17.4 9.3-10.7 28 7.2 35.7 12 2 1.1 11 6.9 11.4 1.1.4-5.2-10-8.2-13.5-10-11.1-5.2-30-15.3-35-27.3-2.5-6 2.8-13.8 9.4-13.6 6.9.2 13.4 7 17.5 12C70.9 34 75 43.8 86.3 47.4z"/> </svg> </span> <span class="webName">nLab</span> monad (in computer science) </h1> <div class="navigation"> <span class="skipNav"><a href='#navEnd'>Skip the Navigation Links</a> | </span> <span style="display:inline-block; width: 0.3em;"></span> <a href="/nlab/show/HomePage" accesskey="H" title="Home page">Home Page</a> | <a href="/nlab/all_pages" accesskey="A" title="List of all pages">All Pages</a> | <a href="/nlab/latest_revisions" accesskey="U" title="Latest edits and page creations">Latest Revisions</a> | <a href="https://nforum.ncatlab.org/discussion/15359/#Item_47" title="Discuss this page in its dedicated thread on the nForum" style="color: black">Discuss this page</a> | <form accept-charset="utf-8" action="/nlab/search" id="navigationSearchForm" method="get"> <fieldset class="search"><input type="text" id="searchField" name="query" value="Search" style="display:inline-block; float: left;" onfocus="this.value == 'Search' ? this.value = '' : true" onblur="this.value == '' ? this.value = 'Search' : true" /></fieldset> </form> <span id='navEnd'></span> </div> <div id="revision"> <html xmlns="http://www.w3.org/1999/xhtml" xmlns:svg="http://www.w3.org/2000/svg" xml:lang="en" lang="en"> <head><meta http-equiv="Content-type" content="application/xhtml+xml;charset=utf-8" /><title>Contents</title></head> <body> <blockquote> <p>This entry is about <a class="existingWikiWord" href="/nlab/show/monads">monads</a> as known from <a class="existingWikiWord" href="/nlab/show/categorical+algebra">categorical algebra</a> but in their application to <a class="existingWikiWord" href="/nlab/show/computer+science">computer science</a>. See also at <em><a class="existingWikiWord" href="/nlab/show/monad+%28disambiguation%29">monad (disambiguation)</a></em>.</p> </blockquote> <hr /> <div class="rightHandSide"> <div class="toc clickDown" tabindex="0"> <h3 id="context">Context</h3> <h4 id="computation">Computation</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/constructive+mathematics">constructive mathematics</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/realizability">realizability</a></strong>, <strong><a class="existingWikiWord" href="/nlab/show/computability">computability</a></strong></p> <p><a class="existingWikiWord" href="/nlab/show/intuitionistic+mathematics">intuitionistic mathematics</a></p> <p><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>, <a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>, <a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></p> <h3 id="constructive_mathematics">Constructive mathematics</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/topos">topos</a>, <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-topos">homotopy topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/canonical+form">canonical form</a>, <a class="existingWikiWord" href="/nlab/show/univalence">univalence</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>, <a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/decidable+equality">decidable equality</a>, <a class="existingWikiWord" href="/nlab/show/decidable+subset">decidable subset</a>, <a class="existingWikiWord" href="/nlab/show/inhabited+set">inhabited set</a>, <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></p> </li> </ul> <h3 id="realizability">Realizability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+topos">realizability topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+model">realizability model</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/realizability+interpretation">realizability interpretation</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/effective+topos">effective topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kleene%27s+first+algebra">Kleene's first algebra</a>, <a class="existingWikiWord" href="/nlab/show/Kleene%27s+second+algebra">Kleene's second algebra</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/function+realizability">function realizability</a></p> </li> </ul> <h3 id="computability">Computability</h3> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/computability">computability</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computation">computation</a>, <a class="existingWikiWord" href="/nlab/show/computational+type+theory">computational type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function">computable function</a>, <a class="existingWikiWord" href="/nlab/show/partial+recursive+function">partial recursive function</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+analysis">computable analysis</a>, <a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Type+Two+Theory+of+Effectivity">Type Two Theory of Effectivity</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+function+%28analysis%29">computable function (analysis)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/exact+real+computer+arithmetic">exact real computer arithmetic</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+set">computable set</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/persistent+homology">persistent homology</a>, <a class="existingWikiWord" href="/nlab/show/effective+homology">effective homology</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/computable+physics">computable physics</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Church-Turing+thesis">Church-Turing thesis</a></p> </li> </ul> </div></div> <h4 id="categorical_algebra">Categorical algebra</h4> <div class="hide"><div> <p><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>+<a class="existingWikiWord" href="/nlab/show/algebra">algebra</a></p> <p><strong><a class="existingWikiWord" href="/nlab/show/internalization">internalization</a> and <a class="existingWikiWord" href="/nlab/show/categorical+algebra">categorical algebra</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/monoid+object">monoid object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/group+object">group object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/ring+object">ring object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+object">algebra object</a> (associative, <a class="existingWikiWord" href="/nlab/show/Lie+algebra+object">Lie</a>, …)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/module+object">module object</a>/<a class="existingWikiWord" href="/nlab/show/action+object">action object</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+locale">internal locale</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+category">internal category</a> (<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>→</mo></mrow><annotation encoding="application/x-tex">\to</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/internal+infinity-categories+contents">more</a>)</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+groupoid">internal groupoid</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+site">internal site</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+diagram">internal diagram</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/universal+algebra">universal algebra</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+over+a+Lawvere+theory">algebras over</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/algebraic+theories">algebraic theories</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+over+a+monad">algebras over</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/monads">monads</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/algebra+over+an+operad">algebras over</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/operads">operads</a></p> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/internal+language">internal language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+category+theory+and+type+theory">relation between category theory and type theory</a></p> </li> </ul> </div></div> <h4 id="type_theory">Type theory</h4> <div class="hide"><div> <p><strong><a class="existingWikiWord" href="/nlab/show/natural+deduction">natural deduction</a></strong> <a class="existingWikiWord" href="/nlab/show/metalanguage">metalanguage</a>, <a class="existingWikiWord" href="/nlab/show/practical+foundations">practical foundations</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/judgement">judgement</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/hypothetical+judgement">hypothetical judgement</a>, <a class="existingWikiWord" href="/nlab/show/sequent">sequent</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/antecedents">antecedents</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊢</mo></mrow><annotation encoding="application/x-tex">\vdash</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/consequent">consequent</a>, <a class="existingWikiWord" href="/nlab/show/succedents">succedents</a></li> </ul> </li> </ul> <ol> <li><a class="existingWikiWord" href="/nlab/show/type+formation+rule">type formation rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+introduction+rule">term introduction rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/term+elimination+rule">term elimination rule</a></li> <li><a class="existingWikiWord" href="/nlab/show/computation+rule">computation rule</a></li> </ol> <p><strong><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></strong> (<a class="existingWikiWord" href="/nlab/show/dependent+type+theory">dependent</a>, <a class="existingWikiWord" href="/nlab/show/intensional+type+theory">intensional</a>, <a class="existingWikiWord" href="/nlab/show/observational+type+theory">observational type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>)</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/calculus+of+constructions">calculus of constructions</a></li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/syntax">syntax</a></strong> <a class="existingWikiWord" href="/nlab/show/object+language">object language</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/theory">theory</a>, <a class="existingWikiWord" href="/nlab/show/axiom">axiom</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>/<a class="existingWikiWord" href="/nlab/show/type">type</a> (<a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/definition">definition</a>/<a class="existingWikiWord" href="/nlab/show/proof">proof</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a> (<a class="existingWikiWord" href="/nlab/show/proofs+as+programs">proofs as programs</a>)</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/theorem">theorem</a></p> </li> </ul> <div> <p><strong><a class="existingWikiWord" href="/nlab/show/computational+trinitarianism">computational trinitarianism</a></strong> = <br /> <strong><a class="existingWikiWord" href="/nlab/show/propositions+as+types">propositions as types</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/programs+as+proofs">programs as proofs</a></strong> +<strong><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation type theory/category theory</a></strong></p> <table><thead><tr><th><a class="existingWikiWord" href="/nlab/show/logic">logic</a></th><th><a class="existingWikiWord" href="/nlab/show/set+theory">set theory</a> (<a class="existingWikiWord" href="/nlab/show/internal+logic+of+set+theory">internal logic</a> of)</th><th><a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a></th><th><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></th></tr></thead><tbody><tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object">object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/predicate">predicate</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/family+of+sets">family of sets</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/display+morphism">display morphism</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+type">dependent type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof">proof</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/element">element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/generalized+element">generalized element</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/term">term</a>/<a class="existingWikiWord" href="/nlab/show/program">program</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+rule">cut rule</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/composition">composition</a> of <a class="existingWikiWord" href="/nlab/show/classifying+morphisms">classifying morphisms</a> / <a class="existingWikiWord" href="/nlab/show/pullback">pullback</a> of <a class="existingWikiWord" href="/nlab/show/display+maps">display maps</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/substitution">substitution</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/introduction+rule">introduction rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/counit">counit</a> for hom-tensor adjunction</td><td style="text-align: left;">lambda</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/elimination+rule">elimination rule</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/unit">unit</a> for hom-tensor adjunction</td><td style="text-align: left;">application</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cut+elimination">cut elimination</a> for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">one of the <a class="existingWikiWord" href="/nlab/show/zigzag+identities">zigzag identities</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/beta+reduction">beta reduction</a></td></tr> <tr><td style="text-align: left;">identity elimination for <a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"></td><td style="text-align: left;">the other <a class="existingWikiWord" href="/nlab/show/zigzag+identity">zigzag identity</a> for hom-tensor adjunction</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/eta+conversion">eta conversion</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/true">true</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/singleton">singleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-2%29-truncated+object">(-2)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+0">h-level 0</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/false">false</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proposition">proposition</a>, <a class="existingWikiWord" href="/nlab/show/truth+value">truth value</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncated+object">(-1)-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>, <a class="existingWikiWord" href="/nlab/show/mere+proposition">mere proposition</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+conjunction">logical conjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product">product</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/product+type">product type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjunction">disjunction</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/sum+type">sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/implication">implication</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> (into <a class="existingWikiWord" href="/nlab/show/subsingleton">subsingleton</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> (into <a class="existingWikiWord" href="/nlab/show/subterminal+object">subterminal object</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> (into <a class="existingWikiWord" href="/nlab/show/h-proposition">h-proposition</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/negation">negation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+set">function set</a> into <a class="existingWikiWord" href="/nlab/show/empty+set">empty set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> into <a class="existingWikiWord" href="/nlab/show/initial+object">initial object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/function+type">function type</a> into <a class="existingWikiWord" href="/nlab/show/empty+type">empty type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universal+quantification">universal quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/cartesian+product">cartesian product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subsingletons">subsingletons</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product">dependent product</a> (of family of <a class="existingWikiWord" href="/nlab/show/subterminal+objects">subterminal objects</a>)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+product+type">dependent product type</a> (of family of <a class="existingWikiWord" href="/nlab/show/h-propositions">h-propositions</a>)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/existential+quantification">existential quantification</a></td><td style="text-align: left;">indexed <a class="existingWikiWord" href="/nlab/show/disjoint+union">disjoint union</a> (<a class="existingWikiWord" href="/nlab/show/support">support</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum">dependent sum</a> (<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a> of)</td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/dependent+sum+type">dependent sum type</a> (<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a> of)</td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/logical+equivalence">logical equivalence</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/bijection+set">bijection set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+of+isomorphisms">object of isomorphisms</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+type">equivalence type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+set">support set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/support+object">support object</a>/<a class="existingWikiWord" href="/nlab/show/%28-1%29-truncation">(-1)-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/propositional+truncation">propositional truncation</a>/<a class="existingWikiWord" href="/nlab/show/bracket+type">bracket type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-image">n-image</a> of <a class="existingWikiWord" href="/nlab/show/morphism">morphism</a> into <a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a>/<a class="existingWikiWord" href="/nlab/show/n-truncation">n-truncation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/n-truncation+modality">n-truncation modality</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equality">equality</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/diagonal+function">diagonal function</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+subset">diagonal subset</a>/<a class="existingWikiWord" href="/nlab/show/diagonal+relation">diagonal relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/path+space+object">path space object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/identity+type">identity type</a>/<a class="existingWikiWord" href="/nlab/show/path+type">path type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/completely+presented+set">completely presented set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/discrete+object">discrete object</a>/<a class="existingWikiWord" href="/nlab/show/0-truncated+object">0-truncated object</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/h-level+2">h-level 2</a>-<a class="existingWikiWord" href="/nlab/show/type">type</a>/<a class="existingWikiWord" href="/nlab/show/set">set</a>/<a class="existingWikiWord" href="/nlab/show/h-set">h-set</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> with <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/groupoid+object+in+an+%28infinity%2C1%29-category">internal 0-groupoid</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/Bishop+set">Bishop set</a>/<a class="existingWikiWord" href="/nlab/show/setoid">setoid</a> with its <a class="existingWikiWord" href="/nlab/show/pseudo-equivalence+relation">pseudo-equivalence relation</a> an actual <a class="existingWikiWord" href="/nlab/show/equivalence+relation">equivalence relation</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/equivalence+class">equivalence class</a>/<a class="existingWikiWord" href="/nlab/show/quotient+set">quotient set</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient">quotient</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+type">quotient type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/colimit">colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/inductive+type">inductive type</a>, <a class="existingWikiWord" href="/nlab/show/W-type">W-type</a>, <a class="existingWikiWord" href="/nlab/show/M-type">M-type</a></td></tr> <tr><td style="text-align: left;">higher <a class="existingWikiWord" href="/nlab/show/induction">induction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/higher+inductive+type">higher inductive type</a></td></tr> <tr><td style="text-align: left;">-</td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/0-truncated">0-truncated</a> <a class="existingWikiWord" href="/nlab/show/%28infinity%2C1%29-colimit">higher colimit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quotient+inductive+type">quotient inductive type</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinduction">coinduction</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/limit">limit</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/coinductive+type">coinductive type</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/preset">preset</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type">type</a> without <a class="existingWikiWord" href="/nlab/show/identity+types">identity types</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/truth+values">truth values</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/subobject+classifier">subobject classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+of+propositions">type of propositions</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+of+discourse">domain of discourse</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/universe">universe</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/object+classifier">object classifier</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modality">modality</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/closure+operator">closure operator</a>, (<a class="existingWikiWord" href="/nlab/show/idempotent+monad">idempotent</a>) <a class="existingWikiWord" href="/nlab/show/monad">monad</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>, <a class="existingWikiWord" href="/nlab/show/monad+%28in+computer+science%29">monad (in computer science)</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+logic">linear logic</a></td><td style="text-align: left;"></td><td style="text-align: left;">(<a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+category">symmetric</a>, <a class="existingWikiWord" href="/nlab/show/closed+monoidal+category">closed</a>) <a class="existingWikiWord" href="/nlab/show/monoidal+category">monoidal category</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>/<a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a></td></tr> <tr><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/proof+net">proof net</a></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/string+diagram">string diagram</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/quantum+circuit">quantum circuit</a></td></tr> <tr><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/contraction+rule">contraction rule</a></td><td style="text-align: left;"></td><td style="text-align: left;">(absence of) <a class="existingWikiWord" href="/nlab/show/diagonal">diagonal</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/no-cloning+theorem">no-cloning theorem</a></td></tr> <tr><td style="text-align: left;"></td><td style="text-align: left;"></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/synthetic+mathematics">synthetic mathematics</a></td><td style="text-align: left;"><a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a></td></tr> </tbody></table> </div> <p><strong><a class="existingWikiWord" href="/nlab/show/homotopy+levels">homotopy levels</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/2-type+theory">2-type theory</a>, <a class="existingWikiWord" href="/michaelshulman/show/2-categorical+logic">2-categorical logic</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a>, <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory+-+contents">homotopy type theory - contents</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/homotopy+type">homotopy type</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/univalence">univalence</a>, <a class="existingWikiWord" href="/nlab/show/function+extensionality">function extensionality</a>, <a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/directed+homotopy+type+theory">directed homotopy type theory</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/HoTT+methods+for+homotopy+theorists">HoTT methods for homotopy theorists</a></p> </li> </ul> </li> </ul> <p><strong><a class="existingWikiWord" href="/nlab/show/semantics">semantics</a></strong></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic">internal logic</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/display+map">display map</a></li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+a+topos">internal logic of a topos</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Mitchell-Benabou+language">Mitchell-Benabou language</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Kripke-Joyal+semantics">Kripke-Joyal semantics</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/internal+logic+of+an+%28%E2%88%9E%2C1%29-topos">internal logic of an (∞,1)-topos</a></p> <ul> <li><a class="existingWikiWord" href="/nlab/show/type-theoretic+model+category">type-theoretic model category</a></li> </ul> </li> </ul> <div> <p> <a href="/nlab/edit/type+theory+-+contents">Edit this sidebar</a> </p> </div></div></div> </div> </div> <h1 id="contents">Contents</h1> <div class='maruku_toc'> <ul> <li><a href='#Idea'>Idea</a></li> <ul> <li><a href='#BasicIdea'>Basic idea: Monadic effects</a></li> <li><a href='#RefinedIdea'>Refined idea: Strong monads</a></li> <li><a href='#MonadModulesInIdeaSection'>Further idea: Monad modules</a></li> <li><a href='#DualIdeaComonadicCauses'>Dual idea: Comonadic contexts</a></li> <li><a href='#DoNotation'>Syntactic idea: Do-notation</a></li> </ul> <li><a href='#Examples'>Examples</a></li> <ul> <li><a href='#definable_monads'>Definable monads</a></li> <ul> <li><a href='#StateMonad'>State monad and Random access memory</a></li> <li><a href='#maybe_monad_and_controlled_failure'>Maybe monad and Controlled failure</a></li> <li><a href='#exception_monad_and_exception_handling'>Exception monad and Exception handling</a></li> <li><a href='#continuation_monad_and_continuationpassing'>Continuation monad and Continuation-passing</a></li> </ul> <li><a href='#axiomatic_monads'>Axiomatic monads</a></li> </ul> <li><a href='#related_concepts'>Related concepts</a></li> <li><a href='#references'>References</a></li> <ul> <li><a href='#ReferencesGeneral'>General</a></li> <li><a href='#in_quantum_computation'>In quantum computation</a></li> </ul> </ul> </div> <h2 id="Idea">Idea</h2> <p>In <a class="existingWikiWord" href="/nlab/show/computer+science">computer science</a>, a <em>(<a class="existingWikiWord" href="/nlab/show/comonad">co-</a>)<a class="existingWikiWord" href="/nlab/show/monad">monad</a></em> (or <em>(<a class="existingWikiWord" href="/nlab/show/co-Kleisli+category">co-</a>)<a class="existingWikiWord" href="/nlab/show/Kleisli+triple">Kleisli triple</a></em>, or <em>(co-)<a class="existingWikiWord" href="/nlab/show/extension+system">extension system</a></em>) is a kind of <a class="existingWikiWord" href="/nlab/show/data+type">data type</a>-structure which describes “notions of computations” [<a href="#Moggi89">Moggi (1989)</a>, <a href="#Moggi91">Moggi (1991)</a>] that may “have external effects or be subject to external contexts/causes” — such as involving <a class="existingWikiWord" href="/nlab/show/random+access+memory">random access memory</a>, <a class="existingWikiWord" href="/nlab/show/IO-monad">input/output</a>, <a class="existingWikiWord" href="/nlab/show/exception+monad">exception handling</a>, <a class="existingWikiWord" href="/nlab/show/writer+monad">writing to</a> or <a class="existingWikiWord" href="/nlab/show/reader+monad">reading from</a> global variables, etc. — as familiar from <a class="existingWikiWord" href="/nlab/show/imperative+programming">imperative programming</a> but cast as “pure functions” with deterministic and <a class="existingWikiWord" href="/nlab/show/verified+programming">verifiable behaviour</a>, in the style of <a class="existingWikiWord" href="/nlab/show/functional+programming">functional programming</a>.</p> <p>In short, a (“<a class="existingWikiWord" href="/nlab/show/extension+system">extension system</a>-style” [<a href="#Manes76">Manes (1976), Ex. 3.12</a>] or “<a class="existingWikiWord" href="/nlab/show/Kleisli+triple">Kleisli triple</a>-style” [<a href="#Moggi91">Moggi (1991), Def. 1.2</a>]) <em><a class="existingWikiWord" href="/nlab/show/monad">monad</a></em> in a given <a class="existingWikiWord" href="/nlab/show/programming+language">programming language</a> consists of <em>assignments</em> (but see <a href="#RefinedIdea">below</a>):</p> <ol> <li> <p>to any <a class="existingWikiWord" href="/nlab/show/data+type">data</a> <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> of a new data type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(D)</annotation></semantics></math> of “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>-data with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects”,</p> </li> <li> <p>to any <a class="existingWikiWord" href="/nlab/show/pair">pair</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful <a class="existingWikiWord" href="/nlab/show/functions">functions</a> (programs) of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mn>12</mn></msub><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">prog_{12} \,\colon\, D_1 \to \mathcal{E}(D_2)</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>3</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">prog_{23} \,\colon\, D_2 \to \mathcal{E}(D_3)</annotation></semantics></math> of an effective-composite function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>12</mn></msub><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>3</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">bind^{\mathcal{E}} prog_{23} \;\circ\; prog_{12}(-) \,\colon\, D_1 \to \mathcal{E}(D_3)</annotation></semantics></math> (their <em>binding</em> or <em><a class="existingWikiWord" href="/nlab/show/Kleisli+composition">Kleisli composition</a></em>),</p> </li> <li> <p>to any <a class="existingWikiWord" href="/nlab/show/data+type">data</a> <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> of a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>ret</mi> <mi>D</mi> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>D</mi><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D)</annotation></semantics></math> assigning “trivial <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects”,</p> </li> </ol> <p>such that the binding is <a class="existingWikiWord" href="/nlab/show/associativity">associative</a> and also <a class="existingWikiWord" href="/nlab/show/unitality">unital</a> with respect to the return operation, hence such that <a class="existingWikiWord" href="/nlab/show/data+types">data types</a> with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful programs between them constitute a <a class="existingWikiWord" href="/nlab/show/category">category</a> (the <em><a class="existingWikiWord" href="/nlab/show/Kleisli+category">Kleisli category</a></em> of the given effect/monad <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>).</p> <p>We now explain in more detail what this means and what it is good for.</p> <h3 id="BasicIdea">Basic idea: Monadic effects</h3> <p>In <a class="existingWikiWord" href="/nlab/show/programming+language">programming</a> it frequently happens that a <a class="existingWikiWord" href="/nlab/show/program">program</a> with “nominal” output <a class="existingWikiWord" href="/nlab/show/data+type">data type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> <em>de facto</em> outputs data of some modified type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>T</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">T(D)</annotation></semantics></math> which accounts for “external effects” caused by the program, where</p> <div class="maruku-equation" id="eq:MonadMapInIntroduction"><span class="maruku-eq-number">(1)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>D</mi><mspace width="thickmathspace"></mspace><mo>↦</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> D \;\mapsto\; \mathcal{E}(D) </annotation></semantics></math></div> <p>is some general operation sending <a class="existingWikiWord" href="/nlab/show/data+types">data types</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> to new data types <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(D)</annotation></semantics></math>.</p> <blockquote> <p>For example, if alongside the computation of its nominal output data <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>d</mi><mo lspace="verythinmathspace">:</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">d \colon D</annotation></semantics></math> a program also writes a log message <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>msg</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">msg \,\colon\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/String+%28computer+science%29">String</a>, then its actual output data is the <a class="existingWikiWord" href="/nlab/show/pair">pair</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">(</mo><mi>d</mi><mo>,</mo><mi>msg</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">(d, msg)</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/product+type">product type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Write</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>≔</mo><mspace width="thinmathspace"></mspace><mi>D</mi><mo>×</mo><mi>String</mi></mrow><annotation encoding="application/x-tex">Write(D) \,\coloneqq\, D \times String</annotation></semantics></math>.</p> <p>Or, dually, if the program may fail and instead “throw an <a class="existingWikiWord" href="/nlab/show/exception">exception</a> message” <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>msg</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">msg \,\colon\,</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/String+%28computer+science%29">String</a>, then its actual output data is <em>either</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>d</mi><mo lspace="verythinmathspace">:</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">d \colon D</annotation></semantics></math> <em>or</em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>msg</mi><mo lspace="verythinmathspace">:</mo><mi>String</mi></mrow><annotation encoding="application/x-tex">msg \colon String</annotation></semantics></math>, hence is of <a class="existingWikiWord" href="/nlab/show/coproduct+type">coproduct type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Excep</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>≔</mo><mspace width="thinmathspace"></mspace><mi>D</mi><mo>⊔</mo><mi>String</mi></mrow><annotation encoding="application/x-tex">Excep(D) \,\coloneqq\, D \sqcup String</annotation></semantics></math>.</p> </blockquote> <p>Given such an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful program <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mn>12</mn></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">prog_{12} \;\colon\; D_1 \to \mathcal{E}(D_2)</annotation></semantics></math> and given a subsequent program <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>3</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">prog_{23} \,\colon\, D_2 \to \mathcal{E}(D_3)</annotation></semantics></math> accepting nominal input data of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">D_2</annotation></semantics></math> and itself possibly involved in further effects of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(-)</annotation></semantics></math>, then the <em>naïve</em> <a class="existingWikiWord" href="/nlab/show/composition">composition</a> of the two programs makes no sense (unless <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>=</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}(D) = D</annotation></semantics></math> is actually the trivial sort of effect), but their evident <em>intended</em> composition is, clearly, obtained by:</p> <ol> <li> <p>first adjusting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mn>23</mn></msub></mrow><annotation encoding="application/x-tex">prog_{23}</annotation></semantics></math> via a given prescription</p> <div class="maruku-equation" id="eq:BindingLawInIntroduction"><span class="maruku-eq-number">(2)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mspace width="negativethinmathspace"></mspace><mi>prog</mi><mspace width="thickmathspace"></mspace><mo>↦</mo><mspace width="thickmathspace"></mspace><msup><mi>bind</mi> <mi>ℰ</mi></msup><mi>prog</mi><mspace width="thinmathspace"></mspace><mo>,</mo></mrow><annotation encoding="application/x-tex"> \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! prog \;\mapsto\; bind^{\mathcal{E}} prog \,, </annotation></semantics></math></div> <p>such that <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>3</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">bind^{\mathcal{E}} prog_{23} \,\colon\, \mathcal{E}(D_2) \to \mathcal{E}(D_3)</annotation></semantics></math>:</p> <ol> <li> <p>does accept data of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(D_2)</annotation></semantics></math> and</p> </li> <li> <p>“acts as <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mn>23</mn></msub></mrow><annotation encoding="application/x-tex">prog_{23}</annotation></semantics></math> while <em>carrying</em> any previous <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects along” (this intuition becomes a formal fact below in <a class="maruku-eqref" href="#eq:FreeEffectHandlingIsBinding">(9)</a>);</p> </li> </ol> </li> <li> <p>then forming the naive <a class="existingWikiWord" href="/nlab/show/composition">composition</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>12</mn></msub></mrow><annotation encoding="application/x-tex">bind^{\mathcal{E}} prog_{23} \;\circ\; prog_{12}</annotation></semantics></math></p> </li> </ol> <p id="BindAndReturnGraphics"> as follows:</p> <div style="margin: -20px 0px 20px 10px"> <img src="/nlab/files/KleisliCompositionOfEffectfulPrograms-230927.jpg" width="840px" /> </div> <blockquote> <p>(Beware that we are denoting by “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>ℰ</mi></msup><mi>prog</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">bind^{\mathcal{E}} prog (-)</annotation></semantics></math>” what in <a class="existingWikiWord" href="/nlab/show/programming+languages">programming languages</a> like <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a> <a href="https://wiki.haskell.org/Monad#The_Monad_class">is denoted by</a> “<code>(-) >>= prog</code>” aka “fish notation”, eg. <a href="#Milewski19">Milewski 2019 p. 321</a>, and which some authors denote by an upper-star, “<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>prog</mi> <mo>*</mo></msup><mspace width="thinmathspace"></mspace></mrow><annotation encoding="application/x-tex">prog^\ast\,</annotation></semantics></math>”, e.g. <a href="#Moggi91">Moggi (1991)</a>; <a href="#Uustalu21Lecture1">Uustalu (2021), lecture 1</a>, <a href="https://cs.ioc.ee/~tarmo/mgs21/mgs1.pdf#page=12">p. 12</a>.)</p> </blockquote> <p>Depending on the intended behaviour of these programs, it remains to specify how exactly <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>23</mn></msub></mrow><annotation encoding="application/x-tex">bind^{\mathcal{E}} prog_{23}</annotation></semantics></math> “carries <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(-)</annotation></semantics></math>-effects along”, hence what the “bind” operation <a class="maruku-eqref" href="#eq:BindingLawInIntroduction">(2)</a> does concretely.</p> <blockquote> <p>For instance, in the above example of a logging-effect, where <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Write</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>≔</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo>×</mo><mi>String</mi></mrow><annotation encoding="application/x-tex">Write(D_2) \,\coloneqq\, D_2 \times String</annotation></semantics></math>, the evident way is to use the <a class="existingWikiWord" href="/nlab/show/concatenation">concatenation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>String</mi><mo>×</mo><mi>String</mi><mover><mo>→</mo><mrow><mspace width="thickmathspace"></mspace><mi>concat</mi><mspace width="thickmathspace"></mspace></mrow></mover><mi>String</mi></mrow><annotation encoding="application/x-tex">String \times String \xrightarrow{\; concat \;} String</annotation></semantics></math> and set:</p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>Write</mi></msup><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo>×</mo><mi>String</mi><mover><mo>→</mo><mrow><msub><mi>prog</mi> <mn>23</mn></msub><mo>×</mo><msub><mi>Id</mi> <mi>String</mi></msub></mrow></mover><msub><mi>D</mi> <mn>3</mn></msub><mo>×</mo><mi>String</mi><mo>×</mo><mi>String</mi><mover><mo>→</mo><mrow><msub><mi>Id</mi> <mrow><msub><mi>D</mi> <mn>3</mn></msub></mrow></msub><mo>×</mo><mi>concat</mi></mrow></mover><msub><mi>D</mi> <mn>3</mn></msub><mo>×</mo><mi>String</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> bind^{Write} prog_{23}\;\coloneqq\; D_2 \times String \xrightarrow{ prog_{23} \times Id_{String} } D_3 \times String \times String \xrightarrow{ Id_{D_3} \times concat } D_3 \times String \,. </annotation></semantics></math></p> <p>In the other example above, where the effect is the possible throwing of an <a class="existingWikiWord" href="/nlab/show/exception">exception</a> message, the evident way to carry this kind of effect along is to use the <a class="existingWikiWord" href="/nlab/show/codiagonal">codiagonal</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∇</mo><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>String</mi><mo>⊔</mo><mi>String</mi><mo>→</mo><mi>String</mi></mrow><annotation encoding="application/x-tex">\nabla \,\colon\, String \sqcup String \to String</annotation></semantics></math>, which amounts to keep forwarding the exception that has already been thrown, if any:</p> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>Excep</mi></msup><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo>⊔</mo><mi>String</mi><mover><mo>→</mo><mrow><msub><mi>prog</mi> <mn>23</mn></msub><mo>⊔</mo><msub><mi>Id</mi> <mi>String</mi></msub></mrow></mover><msub><mi>D</mi> <mn>3</mn></msub><mo>⊔</mo><mi>String</mi><mo>⊔</mo><mi>String</mi><mover><mo>→</mo><mrow><msub><mi>id</mi> <mrow><msub><mi>D</mi> <mn>3</mn></msub></mrow></msub><mo>⊔</mo><mo>∇</mo></mrow></mover><msub><mi>D</mi> <mn>3</mn></msub><mo>⊔</mo><mi>String</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex">bind^{Excep} prog_{23} \;\coloneqq\; D_2 \sqcup String \xrightarrow{ prog_{23} \sqcup Id_{String} } D_3 \sqcup String \sqcup String \xrightarrow{ id_{D_3} \sqcup \nabla } D_3 \sqcup String \,.</annotation></semantics></math></p> </blockquote> <p>Whatever design choice one makes for how to “carry along effects”, it must be consistent in that applying the method to a <a class="existingWikiWord" href="/nlab/show/triple">triple</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful programs which are nominally composable, then their effectful composition should be unambiguously defined in that it is <a class="existingWikiWord" href="/nlab/show/associative">associative</a>, satisfying the following <a class="existingWikiWord" href="/nlab/show/equation">equation</a> – here called the the first “monad law”:</p> <div class="maruku-equation" id="eq:AssociativityConditionInIntroduction"><span class="maruku-eq-number">(3)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>34</mn></msub><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><mo maxsize="1.8em" minsize="1.8em">(</mo><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>23</mn></msub><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>12</mn></msub><mo maxsize="1.8em" minsize="1.8em">)</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>=</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><msup><mi>bind</mi> <mi>ℰ</mi></msup><mo maxsize="1.8em" minsize="1.8em">(</mo><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>34</mn></msub><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>23</mn></msub><mo maxsize="1.8em" minsize="1.8em">)</mo><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>12</mn></msub><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> bind^{\mathcal{E}} prog_{34} \;\circ\; \Big( bind^{\mathcal{E}} prog_{23} \;\circ\; prog_{12} \Big) \;\;\;=\;\;\; bind^{\mathcal{E}} \Big( bind^{\mathcal{E}} prog_{34} \;\circ\; prog_{23} \Big) \;\circ\; prog_{12} \,. </annotation></semantics></math></div> <p>Finally, for such a notion of effectful programs to be usefully connected to “pure” programs without effects, it ought to be the case that for any program <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mn>01</mn></msub><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>0</mn></msub><mover><mo>→</mo><mspace width="thickmathspace"></mspace></mover><msub><mi>D</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">prog_{01} \,\colon\, D_0 \xrightarrow{\;} D_1</annotation></semantics></math> that happens to have no <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects, we have a prescription for how to regard it as an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful program in a trivial way. For that purpose there should be defined an operation</p> <div class="maruku-equation" id="eq:ReturnMapInIntroduction"><span class="maruku-eq-number">(4)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msub><mi>ret</mi> <mi>D</mi></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>D</mi><mover><mo>→</mo><mspace width="thickmathspace"></mspace></mover><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> ret_{D} \;\colon\; D \xrightarrow{\;} \mathcal{E}(D) </annotation></semantics></math></div> <p>which does nothing but “return” data of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>, but re-regarded as effectful <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(D)</annotation></semantics></math>-data in a trivial way; so that we may construct the trivially effectful program <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>ret</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub></mrow> <mi>𝒟</mi></msubsup><msub><mi>prog</mi> <mn>01</mn></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><msub><mi>D</mi> <mn>0</mn></msub><mover><mo>→</mo><mspace width="thickmathspace"></mspace></mover><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">ret^{\mathcal{D}}_{D_1} prog_{01} \;\colon\; D_0 \xrightarrow{\;} \mathcal{E}(D_1)</annotation></semantics></math>.</p> <blockquote> <p>For instance, in the above example of log-message effects this would be the operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>→</mo><mi>D</mi><mo>×</mo><mi>String</mi></mrow><annotation encoding="application/x-tex">D \to D \times String</annotation></semantics></math> which assigns the <a class="existingWikiWord" href="/nlab/show/empty+set">empty</a> <a class="existingWikiWord" href="/nlab/show/string+%28computer+science%29">string</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>ret</mi> <mi>Write</mi></msup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>d</mi><mo>↦</mo><mo stretchy="false">(</mo><mi>d</mi><mo>,</mo><mo>∅</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">ret^{Write} \;\colon\; d \mapsto (d, \varnothing)</annotation></semantics></math>.</p> <p>In the other example above, of <a class="existingWikiWord" href="/nlab/show/exception+handling">exception handling</a>, the trivial effect <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>→</mo><mi>D</mi><mo>⊔</mo><mi>String</mi></mrow><annotation encoding="application/x-tex">D \to D \sqcup String</annotation></semantics></math> is just not to throw an exception, which is just <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>ret</mi> <mi>Excep</mi></msup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>d</mi><mo>↦</mo><mi>d</mi></mrow><annotation encoding="application/x-tex">ret^{Excep} \;\colon\; d \mapsto d</annotation></semantics></math> (the right <a class="existingWikiWord" href="/nlab/show/coprojection">coprojection</a> into the <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a>).</p> </blockquote> <p>The final consistency condition (i.e. the remaining “monad law”) then is that “carrying along trivial effects is indeed the trivial operation”, i.e. that</p> <div class="maruku-equation" id="eq:UnitalityInIntroduction"><span class="maruku-eq-number">(5)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>prog</mi> <mn>01</mn></msub><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><msub><mi>ret</mi> <mrow><msub><mi>D</mi> <mn>0</mn></msub></mrow></msub><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>=</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>01</mn></msub><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mtext>and</mtext><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><msup><mi>bind</mi> <mi>ℰ</mi></msup><msub><mi>ret</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub></mrow></msub><mspace width="thickmathspace"></mspace><mo>∘</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>01</mn></msub><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo>=</mo><mspace width="thickmathspace"></mspace><msub><mi>prog</mi> <mn>01</mn></msub><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> bind^{\mathcal{E}} prog_{01} \;\circ\; ret_{D_0}(-) \;=\; prog_{01} \;\;\;\;\;\;\;\;\; \text{and} \;\;\;\;\;\;\;\;\; bind^{\mathcal{E}} ret_{D_1} \;\circ\; prog_{01}(-) \;=\; prog_{01} \,. </annotation></semantics></math></div> <p>Notice that the <a class="existingWikiWord" href="/nlab/show/associativity">associativity</a> condition <a class="maruku-eqref" href="#eq:AssociativityConditionInIntroduction">(3)</a> and the <a class="existingWikiWord" href="/nlab/show/unitality">unitality</a> condition <a class="maruku-eqref" href="#eq:UnitalityInIntroduction">(5)</a> are jointly equivalent to saying that <a class="existingWikiWord" href="/nlab/show/data+types">data types</a> with <a class="existingWikiWord" href="/nlab/show/hom-sets">hom-sets</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful programs between them, in the above sense, form a <em><a class="existingWikiWord" href="/nlab/show/category">category</a></em>. In <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> this is known as the <em><a class="existingWikiWord" href="/nlab/show/Kleisli+category">Kleisli category</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Kl</mi><mo stretchy="false">(</mo><mi>ℰ</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Kl(\mathcal{E})</annotation></semantics></math> of a <em><a class="existingWikiWord" href="/nlab/show/monad">monad</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> on the <a class="existingWikiWord" href="/nlab/show/category">category</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Type</mi></mrow><annotation encoding="application/x-tex">Type</annotation></semantics></math> of <a class="existingWikiWord" href="/nlab/show/data+types">data types</a> with programs between them:</p> <div class="maruku-equation" id="eq:TheKleisliCategory"><span class="maruku-eq-number">(6)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mtable displaystyle="false" rowspacing="0.5ex" columnalign="right center left"><mtr><mtd><mi>Obj</mi><mo maxsize="1.8em" minsize="1.8em">(</mo><mi>Kl</mi><mo stretchy="false">(</mo><mi>ℰ</mi><mo stretchy="false">)</mo><mo maxsize="1.8em" minsize="1.8em">)</mo></mtd> <mtd><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>=</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mtd> <mtd><mi>Obj</mi><mo maxsize="1.8em" minsize="1.8em">(</mo><mi>Type</mi><mo maxsize="1.8em" minsize="1.8em">)</mo></mtd></mtr> <mtr><mtd><mi>Hom</mi><mo maxsize="1.8em" minsize="1.8em">(</mo><mi>Kl</mi><mo stretchy="false">(</mo><mi>ℰ</mi><mo stretchy="false">)</mo><mo maxsize="1.8em" minsize="1.8em">)</mo><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo maxsize="1.2em" minsize="1.2em">)</mo></mtd> <mtd><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>=</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mtd> <mtd><mi>Hom</mi><mo maxsize="1.8em" minsize="1.8em">(</mo><mi>Type</mi><mo maxsize="1.8em" minsize="1.8em">)</mo><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo></mtd></mtr> <mtr><mtd><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><msub><mo>∘</mo> <mrow><mi mathvariant="normal">Kl</mi><mo stretchy="false">(</mo><mi>ℰ</mi><mo stretchy="false">)</mo></mrow></msub><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mtd> <mtd><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>=</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mtd> <mtd><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><msub><mo>∘</mo> <mi>Type</mi></msub><msup><mi>bind</mi> <mi>ℰ</mi></msup><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mtd></mtr></mtable></mrow><annotation encoding="application/x-tex"> \begin{array}{rcl} Obj\Big( Kl(\mathcal{E}) \Big) &\;\;=\;\;& Obj\Big( Type \Big) \\ Hom\Big( Kl(\mathcal{E}) \Big)\big(D_1,\, D_2\big) &\;\;=\;\;& Hom\Big( Type \Big) \big( D_1, \, \mathcal{E}(D_2) \big) \\ (-) \circ_{\mathrm{Kl}(\mathcal{E})} (-) &\;\;=\;\;& (-) \circ_{Type} bind^{\mathcal{E}}(-) \,. \end{array} </annotation></semantics></math></div> <blockquote> <p>Traditionally in <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>, the <a class="existingWikiWord" href="/nlab/show/axioms">axioms</a> on <a class="existingWikiWord" href="/nlab/show/monads">monads</a> are presented in a somewhat different way, invoking a monad “product” <a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo>∘</mo><mi>ℰ</mi><mover><mo>→</mo><mi>μ</mi></mover><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E} \circ \mathcal{E} \xrightarrow{ \mu } \mathcal{E}</annotation></semantics></math> instead of the “binding” operation. One readily checks that these two axiomatic presentations of monads are in fact equal – see <a class="maruku-eqref" href="#eq:TransformBetweenBindAndJoinInIntroduction">(7)</a> below –, but the above “<a class="existingWikiWord" href="/nlab/show/Kleisli+triple">Kleisli triple</a>/<a class="existingWikiWord" href="/nlab/show/extension+system">extension system</a>”-presentation is typically more relevant in the practice of <a class="existingWikiWord" href="/nlab/show/functional+programming">functional programming</a>.</p> </blockquote> <p>In summary, a choice of <em>assignments</em> (but see <a href="#RefinedIdea">below</a>) to <a class="existingWikiWord" href="/nlab/show/data+types">data types</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mi>i</mi></msub></mrow><annotation encoding="application/x-tex">D_i</annotation></semantics></math> of</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Type</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}(D) \;\colon\; Type</annotation></semantics></math>,</p> <p>namely of types of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful data of nominal type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> <a class="maruku-eqref" href="#eq:MonadMapInIntroduction">(1)</a>;</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>bind</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>D</mi> <mn>2</mn></msub></mrow> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mo>⟶</mo><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo></mrow><annotation encoding="application/x-tex">bind^{\mathcal{E}}_{D_1, D_2} \;\colon\; Hom\big(D_1,\, \mathcal{E}(D_2)\big) \longrightarrow Hom\big(\mathcal{E}(D_1),\,\mathcal{E}(D_2)\big)</annotation></semantics></math>,</p> <p>namely of how to execute a prog while carrying along any previous effects <a class="maruku-eqref" href="#eq:BindingLawInIntroduction">(2)</a>;</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>ret</mi> <mi>D</mi> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>D</mi><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D)</annotation></semantics></math>,</p> <p>namely of how to regard plain <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>-data as trivially effectful <a class="maruku-eqref" href="#eq:ReturnMapInIntroduction">(4)</a></p> </li> </ol> <p>subject to:</p> <ol> <li> <p>the <a class="existingWikiWord" href="/nlab/show/associativity">associativity</a> condition <a class="maruku-eqref" href="#eq:AssociativityConditionInIntroduction">(3)</a></p> </li> <li> <p>the <a class="existingWikiWord" href="/nlab/show/unitality">unitality</a> condition <a class="maruku-eqref" href="#eq:UnitalityInIntroduction">(5)</a></p> </li> </ol> <p>is called a <em><a class="existingWikiWord" href="/nlab/show/monad+in+computer+science">monad in computer science</a></em> (also: “<a class="existingWikiWord" href="/nlab/show/Kleisli+triple">Kleisli triple</a>” in <a class="existingWikiWord" href="/nlab/show/functional+programming">functional programming</a>) and serves to encode the notion that all programs may be subject to certain <em>external effects</em> of a kind <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> that is specified by the above choices of monad operations.</p> <p>Here, for the time being (but see <a href="#RefinedIdea">below</a>), we write <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Hom</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Hom(D_1, D_2)</annotation></semantics></math> for the <em><a class="existingWikiWord" href="/nlab/show/set">set</a></em> of programs/functions taking data of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">D_1</annotation></semantics></math> to data of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">D_2</annotation></semantics></math> (the <em><a class="existingWikiWord" href="/nlab/show/hom+set">hom set</a></em> in the plain <a class="existingWikiWord" href="/nlab/show/category">category</a> of <a class="existingWikiWord" href="/nlab/show/types">types</a>).</p> <blockquote> <p>The first running example above is known as the <em><a class="existingWikiWord" href="/nlab/show/writer+monad">writer monad</a></em>, since it encodes the situation where programs may have the additional effect of writing a message string into a given buffer.</p> <p>The other running example above is naturally called the <em><a class="existingWikiWord" href="/nlab/show/exception+monad">exception monad</a></em>.</p> </blockquote> <p><br /></p> <p><strong>Relation to other familiar axioms for monads.</strong> The above Kleisli/extension-structure, making a <a class="existingWikiWord" href="/nlab/show/Kleisli+category">Kleisli-style</a> <a class="existingWikiWord" href="/nlab/show/monad+in+computer+science">monad in computer science</a>, may and often is encoded in different equivalent ways:</p> <p>Alternatively postulating operations</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>↦</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">D \mapsto \mathcal{E}(D)</annotation></semantics></math> (as before)</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>fmap</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>D</mi> <mn>2</mn></msub></mrow> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><msub><mi>D</mi> <mn>2</mn></msub><mo maxsize="1.2em" minsize="1.2em">)</mo><mo>⟶</mo><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>,</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo></mrow><annotation encoding="application/x-tex">fmap^{\mathcal{E}}_{D_1, D_2} \;\colon\; Hom\big(D_1 \to D_2\big) \longrightarrow Hom\big(\mathcal{E}(D_1), \mathcal{E}(D_2)\big)</annotation></semantics></math></p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>ret</mi> <mi>D</mi> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>D</mi><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">ret^{\mathcal{E}}_D \;\colon\; D \to \mathcal{E}(D)</annotation></semantics></math></p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msubsup><mi>join</mi> <mi>D</mi> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">join^{\mathcal{E}}_D \;\colon\; \mathcal{E}\big( \mathcal{E}(D) \big) \to \mathcal{E}(D)</annotation></semantics></math></p> </li> </ol> <p>such that</p> <ol> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>fmap</mi> <mi>ℰ</mi></msup></mrow><annotation encoding="application/x-tex">fmap^{\mathcal{E}}</annotation></semantics></math> is <em><a class="existingWikiWord" href="/nlab/show/functor">functorial</a></em> on <a class="existingWikiWord" href="/nlab/show/data+types">data types</a>,</p> </li> <li> <p><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>join</mi> <mi>ℰ</mi></msup></mrow><annotation encoding="application/x-tex">join^{\mathcal{E}}</annotation></semantics></math> is <a class="existingWikiWord" href="/nlab/show/associativity">associative</a> and <a class="existingWikiWord" href="/nlab/show/unitality">unital</a> (with respect to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ret</mi></mrow><annotation encoding="application/x-tex">ret</annotation></semantics></math>) as a <a class="existingWikiWord" href="/nlab/show/natural+transformation">natural transformation</a>,</p> </li> </ol> <p>yields the definition of <em><a class="existingWikiWord" href="/nlab/show/monad">monad</a></em> more traditionally used in <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> (namely as a <a class="existingWikiWord" href="/nlab/show/monoid+object">monoid object</a> <a class="existingWikiWord" href="/nlab/show/internalization">in</a> <a class="existingWikiWord" href="/nlab/show/endofunctors">endofunctors</a>, here on the plain <a class="existingWikiWord" href="/nlab/show/category">category</a> of <a class="existingWikiWord" href="/nlab/show/data+types">data types</a>).</p> <p>Direct inspection shows that one may <a class="existingWikiWord" href="/nlab/show/bijection">bijectively</a> transmute such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>bind</mi></mrow><annotation encoding="application/x-tex">bind</annotation></semantics></math>- and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>join</mi></mrow><annotation encoding="application/x-tex">join</annotation></semantics></math>-operators into each other by expressing them as the following composites (using <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a>-notation, for instance “ev” denotes the <a class="existingWikiWord" href="/nlab/show/evaluation+map">evaluation map</a>):</p> <div class="maruku-equation" id="eq:TransformBetweenBindAndJoinInIntroduction"><span class="maruku-eq-number">(7)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left left"><mtr><mtd></mtd> <mtd><msubsup><mi>fmap</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>D</mi> <mn>2</mn></msub></mrow> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>D</mi> <mn>2</mn></msub><mo maxsize="1.2em" minsize="1.2em">)</mo><mover><mo>→</mo><mrow><mi>ret</mi><mo>∘</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo></mrow></mover><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mover><mo>→</mo><mi>bind</mi></mover><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><msubsup><mi>join</mi> <mi>D</mi> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mover><mo>→</mo><mrow><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>id</mi> <mrow><mi>ℰ</mi><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow></msub><mo>,</mo><mi>name</mi><mo stretchy="false">(</mo><msub><mi>id</mi> <mrow><mi>ℰ</mi><mi>D</mi></mrow></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo></mrow></mover><mi>ℰ</mi><mi>ℰ</mi><mi>D</mi><mo>×</mo><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mover><mo>→</mo><mi>bind</mi></mover><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mtext>and conversely:</mtext></mtd></mtr> <mtr><mtd></mtd> <mtd><msubsup><mi>bind</mi> <mrow><mi>D</mi><mo>,</mo><mi>D</mi><mo>′</mo></mrow> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>×</mo><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>D</mi><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo>′</mo><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mover><mo>→</mo><mrow><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>id</mi> <mrow><mi>ℰ</mi><mi>D</mi></mrow></msub><mo>,</mo><msub><mi>fmap</mi> <mrow><mi>D</mi><mo>,</mo><mi>ℰ</mi><mi>D</mi><mo>′</mo></mrow></msub><mo maxsize="1.2em" minsize="1.2em">)</mo></mrow></mover><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>×</mo><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>,</mo><mi>ℰ</mi><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo>′</mo><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mover><mo>→</mo><mrow><mspace width="thickmathspace"></mspace><mi>ev</mi><mspace width="thickmathspace"></mspace></mrow></mover><mi>ℰ</mi><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo>′</mo><mo stretchy="false">)</mo><mover><mo>→</mo><mrow><mspace width="thickmathspace"></mspace><mi>join</mi><mspace width="thickmathspace"></mspace></mrow></mover><mi>D</mi><mo>′</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mtd></mtr></mtable></mrow><annotation encoding="application/x-tex"> \begin{array}{ll} & fmap^{\mathcal{E}}_{D_1, D_2} \;\colon\; Hom\big(D_1, D_2\big) \xrightarrow{ ret \circ (-) } Hom\big(D_1,\, \mathcal{E}(D_2) \big) \xrightarrow{ bind } Hom\big( \mathcal{E}(D_1),\, \mathcal{E}(D_2) \big) \\ & join^{\mathcal{E}}_D \;\colon\; \mathcal{E}\big( \mathcal{E}(D) \big) \xrightarrow{ \big( id_{ \mathcal{E} \mathcal{E}(D) }, name(id_{ \mathcal{E} D }) \big) } \mathcal{E} \mathcal{E} D \times Hom\big( \mathcal{E}(D),\, \mathcal{E}(D) \big) \xrightarrow{ bind } \mathcal{E}(D) \\ \text{and conversely:} \\ & bind^{\mathcal{E}}_{D, D'} \;\colon\; \mathcal{E}(D) \times Hom\big( D,\, \mathcal{E}(D') \big) \xrightarrow{ \big( id_{\mathcal{E} D}, fmap_{D, \mathcal{E} D'} \big) } \mathcal{E} (D) \times Hom\big( \mathcal{E}(D) , \mathcal{E}\mathcal{E}(D') \big) \xrightarrow{\; ev \;} \mathcal{E} \mathcal{E}(D') \xrightarrow{\; join \;} D' \,. \end{array} </annotation></semantics></math></div> <h3 id="RefinedIdea">Refined idea: Strong monads</h3> <p>But in fact, in <a class="existingWikiWord" href="/nlab/show/functional+programming">functional programming</a>-<a class="existingWikiWord" href="/nlab/show/programming+language">languages</a> one typically considers an enhanced version of the above situation:</p> <p>In these higher-order languages one has, besides the (<a class="existingWikiWord" href="/nlab/show/hom-set">hom-</a>)<em><a class="existingWikiWord" href="/nlab/show/set">set</a></em> of programs/functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Hom</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo maxsize="1.2em" minsize="1.2em">)</mo></mrow><annotation encoding="application/x-tex">Hom\big(D_1, \, D_2\big)</annotation></semantics></math> also the actual <em><a class="existingWikiWord" href="/nlab/show/data+type">data type</a></em> of functions, namely the <em><a class="existingWikiWord" href="/nlab/show/function+type">function type</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><msub><mi>D</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">D_1 \to D_2</annotation></semantics></math>, which in terms of <a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">categorical semantics</a> is the <em><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a>-<a class="existingWikiWord" href="/nlab/show/hom+object">object</a></em> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Map</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">Map(D_1, \, D_2)</annotation></semantics></math> in the <a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed category</a> of <a class="existingWikiWord" href="/nlab/show/data+types">data types</a>. Therefore, in such languages (like <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a>) the <a class="existingWikiWord" href="/nlab/show/type">type</a> of the binding operation for given <a class="existingWikiWord" href="/nlab/show/data+types">data types</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">D_1</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">D_2</annotation></semantics></math> is actually taken to be the <a class="existingWikiWord" href="/nlab/show/function+type">function type</a>/<a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a></p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mtable displaystyle="false" rowspacing="0.5ex" columnalign="left left"><mtr><mtd><msubsup><mi>bind</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>D</mi> <mn>2</mn></msub></mrow> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace></mtd> <mtd></mtd> <mtd><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mo>→</mo><mo maxsize="1.2em" minsize="1.2em">(</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>≃</mo></mtd> <mtd><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>×</mo><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd></mtd> <mtd><mo>≃</mo></mtd> <mtd><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>→</mo><mo maxsize="1.8em" minsize="1.8em">(</mo><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.8em" minsize="1.8em">)</mo></mtd></mtr></mtable></mrow><annotation encoding="application/x-tex"> \begin{array}{ll} bind^{\mathcal{E}}_{D_1, D_2} \;\colon\; && \big( D_1 \to \mathcal{E}(D_2) \big) \to \big( \mathcal{E}(D_1) \to \mathcal{E}(D_2) \big) \\ &\simeq & \mathcal{E}(D_1) \times \big( D_1 \to \mathcal{E}(D_2) \big) \to \mathcal{E}(D_2) \\ & \simeq & \mathcal{E}(D_1) \to \Big( \big( D_1 \to \mathcal{E}(D_2) \big) \to \mathcal{E}(D_2) \Big) \end{array} </annotation></semantics></math></div> <blockquote> <p>(where we used the <a href="adjoint+functor#InTermsOfHomIsomorphism">hom-isomorphism</a> of the <a class="existingWikiWord" href="/nlab/show/product">product</a><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊣</mo></mrow><annotation encoding="application/x-tex">\dashv</annotation></semantics></math><a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a>-<a class="existingWikiWord" href="/nlab/show/adjoint+functors">adjunction</a> to re-identify the <a class="existingWikiWord" href="/nlab/show/types">types</a> on the right)</p> </blockquote> <p>which (beware) is traditionally written without many of the parenthesis, as follows:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msubsup><mi>bind</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msub><mi>D</mi> <mn>2</mn></msub></mrow> <mi>ℰ</mi></msubsup><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><mi>ℰ</mi><msub><mi>D</mi> <mn>2</mn></msub><mo maxsize="1.2em" minsize="1.2em">)</mo><mo>→</mo><mi>ℰ</mi><msub><mi>D</mi> <mn>2</mn></msub><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> bind^{\mathcal{E}}_{D_1, D_2} \;\colon\; \mathcal{E} D_1 \to \big( D_1 \to \mathcal{E} D_2 \big) \to \mathcal{E} D_2 \,. </annotation></semantics></math></div> <p>In general (except in the <a class="existingWikiWord" href="/nlab/show/base+topos">base topos</a> of <a class="existingWikiWord" href="/nlab/show/Sets">Sets</a>), such an iterated <a class="existingWikiWord" href="/nlab/show/function+type">function type</a>/<a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a> is richer than (certainly different from) the corresponding plain <a class="existingWikiWord" href="/nlab/show/hom+set">hom set</a>, and accordingly a “Kleisli triple” defined as above but with the binding operation typed in this <a class="existingWikiWord" href="/nlab/show/internalization">internal</a> way is <em>richer</em> or <em>stronger</em> <a class="existingWikiWord" href="/nlab/show/structure">structure</a> than that of a plain <a class="existingWikiWord" href="/nlab/show/monad">monad</a> on the underlying category of types: namely it is an <em><a class="existingWikiWord" href="/nlab/show/enriched+monad">enriched monad</a></em> or <a href="enriched+monad#RelationToStrongMonads">equivalently</a> a <em><a class="existingWikiWord" href="/nlab/show/strong+monad">strong monad</a></em> with respect to the self-<a class="existingWikiWord" href="/nlab/show/enriched+category">enrichment</a> of the <a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+closed+category">symmetric monoidal closed category</a> of types (<a href="#Moggi91">Moggi 1991 §3</a>, cf. <a href="#GLLN08">Goubault-Larrecq, Lasota & Nowak 2002</a>, <a href="#McDermottUustalu22">McDermott & Uustalu (2022)</a>).</p> <p>On such an <a class="existingWikiWord" href="/nlab/show/enriched+monad">enriched</a>/<a class="existingWikiWord" href="/nlab/show/strong+monad">strong monad</a>, the bind operation is defined as the following composite:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>×</mo><mi>ℰ</mi><mi>Map</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mover><mo>→</mo><mrow><mspace width="thickmathspace"></mspace><msub><mi>strength</mi> <mi>ℰ</mi></msub><mspace width="thickmathspace"></mspace></mrow></mover><mi>ℰ</mi><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>×</mo><mi>Map</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mspace width="thinmathspace"></mspace><mi>ℰ</mi><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.2em" minsize="1.2em">)</mo><mover><mo>→</mo><mrow><mi>ℰ</mi><msub><mi>eval</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><mi>ℰ</mi><msub><mi>D</mi> <mn>2</mn></msub></mrow></msub></mrow></mover><mi>ℰ</mi><mi>ℰ</mi><msub><mi>D</mi> <mn>2</mn></msub><mover><mo>→</mo><mrow><mspace width="thickmathspace"></mspace><msub><mi>μ</mi> <mrow><msub><mi>D</mi> <mn>2</mn></msub></mrow></msub><mspace width="thickmathspace"></mspace></mrow></mover><mi>ℰ</mi><msub><mi>D</mi> <mn>2</mn></msub><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \mathcal{E}(D_1) \times \mathcal{E} Map(D_1,\,D_2) \xrightarrow{\; strength_{\mathcal{E}} \;} \mathcal{E}\big(D_1 \times Map(D_1, \, \mathcal{E} D_2) \big) \xrightarrow{ \mathcal{E} eval_{D_1, \mathcal{E} D_2} } \mathcal{E} \mathcal{E} D_2 \xrightarrow{\; \mu_{D_2} \;} \mathcal{E} D_2 \,. </annotation></semantics></math></div> <p>In particular, monads as used in <a class="existingWikiWord" href="/nlab/show/functional+programming+languages">functional programming languages</a> like <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a> are really strong/enriched monads, in this way.</p> <p>In this case – and in most discussions by default – the <a class="existingWikiWord" href="/nlab/show/symmetric+monoidal+closed+category">symmetric monoidal closed category</a> of types is assumed to be <a class="existingWikiWord" href="/nlab/show/cartesian+closed+category">cartesian closed</a> (“classical types”) but in contexts of <a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a> (such as <a class="existingWikiWord" href="/nlab/show/quantum+computation">quantum computation</a>) it may be non-cartesian (or both: cf. <a class="existingWikiWord" href="/nlab/show/doubly+closed+monoidal+category">doubly closed monoidal category</a>).</p> <p><br /></p> <p>Yet more structure on effect-monads is available in <a class="existingWikiWord" href="/nlab/show/dependent+type+theories">dependent type theories</a> with <a class="existingWikiWord" href="/nlab/show/type+universes">type universes</a>, where one may demand that the monad operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>↦</mo><mi>T</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">D \mapsto T(D)</annotation></semantics></math> is not just an <a class="existingWikiWord" href="/nlab/show/endofunction">endofunction</a> on the <a class="existingWikiWord" href="/nlab/show/set">set</a> of <a class="existingWikiWord" href="/nlab/show/types">types</a>, but an <a class="existingWikiWord" href="/nlab/show/endomorphism">endomorphism</a> of the <a class="existingWikiWord" href="/nlab/show/type+universe">type universe</a>. At least for <a class="existingWikiWord" href="/nlab/show/idempotent+monads">idempotent monads</a> this case is further discussed at <em><a class="existingWikiWord" href="/nlab/show/reflective+subuniverse">reflective subuniverse</a></em> and <em><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a></em> and maybe elsewhere.</p> <h3 id="MonadModulesInIdeaSection">Further idea: Monad modules</h3> <p>Further in the practice of <a class="existingWikiWord" href="/nlab/show/programming+language">programming</a>: if programs may cause external effects, as <a href="#BasicIdea">above</a>, then one will often want to have some of them <em>handle</em> these effects.</p> <blockquote> <p>This is particularly evident in the <a href="#BasicIdea">above</a> running examples of <em><a class="existingWikiWord" href="/nlab/show/exceptions">exceptions</a></em> whose whole design purpose typically is to be handled when they arise.</p> </blockquote> <p>Since a “handling” of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects should mean that these be done with and turned into pure data of some actual <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>, an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect handler on(to) a data type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math> should primarily consist of a program of the form</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>→</mo><mi>D</mi><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> \mathcal{E}(D) \to D \,. </annotation></semantics></math></div> <p>that handles effects produced by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful programs <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>′</mo><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">D' \to \mathcal{E}(D)</annotation></semantics></math>, turning them into pure computations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>′</mo><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex">D' \to D</annotation></semantics></math>.</p> <p>But in addition, such a handler needs to handle effects that have been “carried along” <a class="maruku-eqref" href="#eq:BindingLawInIntroduction">(2)</a> from previous computations, even along otherwise in-effectful computations <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>prog</mi> <mrow><mn>0</mn><mo>,</mo><mn>1</mn></mrow></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><msub><mi>D</mi> <mn>0</mn></msub><mo>→</mo><msub><mi>D</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">prog_{0,1} \;\colon\; D_{0} \to D_{1}</annotation></semantics></math>; therefore all these need to be assigned handlers:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msubsup><mi>hndl</mi> <mrow><msub><mi>D</mi> <mn>2</mn></msub></mrow> <mi>ℰ</mi></msubsup><msub><mi>prog</mi> <mrow><mn>1</mn><mo>,</mo><mn>2</mn></mrow></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>→</mo><msub><mi>D</mi> <mn>2</mn></msub><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> hndl^{\mathcal{E}}_{D_2} prog_{1,2} \;\colon\; \mathcal{E}(D_1) \to D_2 \,. </annotation></semantics></math></div> <p>Of such choice of effect handling, consistency demands that:</p> <ol> <li> <p>first handling all previous effects carried along <a class="maruku-eqref" href="#eq:BindingLawInIntroduction">(2)</a> and then the newly produced effects by a given <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>prog</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><mi>D</mi><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">prog \,\colon\, D \to \mathcal{E}(D')</annotation></semantics></math> has the same result as letting <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>prog</mi></mrow><annotation encoding="application/x-tex">prog</annotation></semantics></math> take care of carrying along previous effects by passing to <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>prog</mi><mo stretchy="false">[</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">prog[-]</annotation></semantics></math> and then handling the resulting accumulation at once:</p> </li> <li> <p>handling the trivial effect ought to be no extra operation:</p> </li> </ol> <div class="maruku-equation" id="eq:AxiomsForEffectHandlers"><span class="maruku-eq-number">(8)</span><code class="maruku-mathml"> </code></div><div style="margin: -20px 0px 20px 10px"> <img src="/nlab/files/MonadicEffectHandlerConditions-221105b.jpg" width="560px" /> </div> <p>A data structure consisting of such assignments <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msup><mi>hndl</mi> <mi>ℰ</mi></msup></mrow><annotation encoding="application/x-tex">hndl^{\mathcal{E}}</annotation></semantics></math> subject to these “laws” is known as an <em>Kleisli triple algebra</em> (e.g. <a href="#Uustalu21Lecture2">Uustalu (2021), Lec. 2</a>) or <em>algebra over an extension system</em> (see <a href="algebra+over+a+monad#ReferencesKleisliStyle">here</a>) for <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> and is bijectively the same as what in traditional <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> is known as an <em><a class="existingWikiWord" href="/nlab/show/algebra+over+a+monad">algebra over <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"> <semantics> <mrow> <mi>ℰ</mi> </mrow> <annotation encoding="application/x-tex">\mathcal{E}</annotation> </semantics> </math></a></em> or <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-algebra</em> or, maybe best: an <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-module</em> or <em><math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/modal+type">modal type</a></em>.</p> <p>Given a <a class="existingWikiWord" href="/nlab/show/pair">pair</a> of such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/modal+types">modal types</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo>,</mo><msubsup><mi>hndl</mi> <mrow><msub><mi>D</mi> <mn>1</mn></msub></mrow> <mi>ℰ</mi></msubsup><mo maxsize="1.2em" minsize="1.2em">)</mo></mrow><annotation encoding="application/x-tex">\big(D_1, hndl^{\mathcal{E}}_{D_1} \big)</annotation></semantics></math>, <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo maxsize="1.2em" minsize="1.2em">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo>,</mo><msubsup><mi>hndl</mi> <mrow><msub><mi>D</mi> <mn>2</mn></msub></mrow> <mi>ℰ</mi></msubsup><mo maxsize="1.2em" minsize="1.2em">)</mo></mrow><annotation encoding="application/x-tex">\big(D_2, hndl^{\mathcal{E}}_{D_2} \big)</annotation></semantics></math>, a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>1</mn></msub><mo>→</mo><msub><mi>D</mi> <mn>2</mn></msub></mrow><annotation encoding="application/x-tex">\phi \,\colon\, D_1 \to D_2</annotation></semantics></math> is a <em><a class="existingWikiWord" href="/nlab/show/homomorphism">homomorphism</a></em> between them if the result of handling <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects before or after applying <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ϕ</mi></mrow><annotation encoding="application/x-tex">\phi</annotation></semantics></math> is the same, hence if for all functions <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>f</mi><mspace width="thinmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thinmathspace"></mspace><msub><mi>D</mi> <mn>0</mn></msub><mo>→</mo><msub><mi>D</mi> <mn>1</mn></msub></mrow><annotation encoding="application/x-tex">f \,\colon\, D_0 \to D_1</annotation></semantics></math> the following <a class="existingWikiWord" href="/nlab/show/commuting+diagram">diagram commutes</a>:</p> <div style="margin: -20px 0px 20px 10px"> <img src="/nlab/files/HomomorphismOfMonadiEffectHandlers-221105.jpg" width="350px" /> </div> <p><br /></p> <p id="FreeModales"> <strong>Free <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect handlers.</strong> Notice that <a href="#BasicIdea">above</a> we motivated already the binding operation <a class="maruku-eqref" href="#eq:BindingLawInIntroduction">(2)</a> as a kind of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect handling: namely as the “carrying along” of previous <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects. This intuition now becomes a precise statement:</p> <p>For any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><msub><mi>D</mi> <mn>2</mn></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>Type</mi></mrow><annotation encoding="application/x-tex">D_2 \;\colon\; Type</annotation></semantics></math> we may tautologically handle <a class="maruku-eqref" href="#eq:AxiomsForEffectHandlers">(8)</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects by absorbing them into the data type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(D_2)</annotation></semantics></math>, with the effect-handler simply being the effect-binding operation <a class="maruku-eqref" href="#eq:BindingLawInIntroduction">(2)</a>:</p> <div class="maruku-equation" id="eq:FreeEffectHandlingIsBinding"><span class="maruku-eq-number">(9)</span><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msubsup><mi>hndl</mi> <mrow><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo></mrow> <mi>ℰ</mi></msubsup><mo maxsize="1.8em" minsize="1.8em">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mover><mo>→</mo><mi>prog</mi></mover><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mo maxsize="1.8em" minsize="1.8em">)</mo><mspace width="thickmathspace"></mspace><mo>≔</mo><mspace width="thickmathspace"></mspace><msup><mi>bind</mi> <mi>ℰ</mi></msup><mi>prog</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>1</mn></msub><mo stretchy="false">)</mo><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><msub><mi>D</mi> <mn>2</mn></msub><mo stretchy="false">)</mo><mspace width="thinmathspace"></mspace><mo>.</mo></mrow><annotation encoding="application/x-tex"> hndl^{\mathcal{E}}_{\mathcal{E}(D_2)} \Big( D_1 \xrightarrow{ prog } \mathcal{E}(D_2) \Big) \;\coloneqq\; bind^{\mathcal{E}} prog \;\colon\; \mathcal{E}(D_1) \to \mathcal{E}(D_2) \,. </annotation></semantics></math></div> <p>The <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect-handlers <a class="maruku-eqref" href="#eq:AxiomsForEffectHandlers">(8)</a> arising this way are called <em><a href="algebra+over+a+monad#FreeAlgebras">free</a></em>.</p> <p>The <a class="existingWikiWord" href="/nlab/show/full+subcategory">full subcategory</a> of free <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect handlers among <a class="existingWikiWord" href="/nlab/show/Eilenberg-Moore+category">all</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-<a class="existingWikiWord" href="/nlab/show/modal+types">modal types</a> is known as the <em><a class="existingWikiWord" href="/nlab/show/Kleisli+category">Kleisli category</a></em>. By the <a href="Kleisli+category#KleisliEquivalence">Kleisli equivalence</a>, this is <a class="existingWikiWord" href="/nlab/show/equivalence+of+categories">equivalent</a> to the (plain) category <a class="maruku-eqref" href="#eq:TheKleisliCategory">(6)</a> of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful programs that we started with. Here this means that:</p> <ul> <li><em>Plain data types with <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful programs betweem them are equivalently data types freely equipped with the structure of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect handlers.</em></li> </ul> <p>which makes a lot of sense.</p> <p><br /></p> <h3 id="DualIdeaComonadicCauses">Dual idea: Comonadic contexts</h3> <div class="float_right_image" style="margin: -40px 0px 20px 30px"> <figure style="margin: 0 0 0 0"> <img src="/nlab/files/Overton-CoMonadHaskell.jpg" width="550px" /> <figcaption style="text-align: center">(from <a href="#Overton14">Overton 2014</a>)</figcaption> </figure> </div> <p>By <a class="existingWikiWord" href="/nlab/show/formal+duality">formal duality</a>, all of the above discussion has a dual version, where now (e.g. <a href="#UustaluVene08">Uustalu & Vene (2008)</a>, <a href="#POM13">POM13</a>, <a href="#GKOBU16">GKOBU16</a>, <a href="#KRU20">KRU20</a>):</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/comonads">comonads</a> encode <em>computational contexts</em> (<em>co-effects</em>),</p> </li> <li> <p>their <a class="existingWikiWord" href="/nlab/show/coproduct">coproduct</a> operation is the <em>duplication</em> (<em>co-join</em>) of contexts which serves to <em>extend</em> (<em>co-bind</em>) contexts over consecutive programs,</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/comodules+over+comonads">comodules over comonads</a> are data structures that <em>provide</em> (<em>co-handle</em>) such context.</p> </li> </ul> <p>In more detail:</p> <ul> <li> <p>Above we had that:</p> <ul> <li> <p>A <a class="existingWikiWord" href="/nlab/show/Kleisli+map">Kleisli map</a> for a <a class="existingWikiWord" href="/nlab/show/monad">monad</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math> is a program</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>prog</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>D</mi><mo>→</mo><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo>′</mo><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> prog \;\colon\; D \to \mathcal{E}(D') </annotation></semantics></math></div> <p><em>causing</em> an external <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect.</p> </li> <li> <p>A Kleisli-module for a <a class="existingWikiWord" href="/nlab/show/monad">monad</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mi>T</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}T</annotation></semantics></math> is a prescription</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msubsup><mi>hdl</mi> <mi>D</mi> <mi>ℰ</mi></msubsup><msub><mi>id</mi> <mi>D</mi></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>→</mo><mi>D</mi></mrow><annotation encoding="application/x-tex"> hdl^{\mathcal{E}}_D id_D \;\colon\; \mathcal{E}(D) \to D </annotation></semantics></math></div> <p>for <em>handling</em> such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effects.</p> </li> </ul> </li> <li> <p>Now dually:</p> <ul> <li> <p>A <a class="existingWikiWord" href="/nlab/show/co-Kleisli+map">co-Kleisli map</a> for a <a class="existingWikiWord" href="/nlab/show/comonad">comonad</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math> is a program</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mi>prog</mi><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>𝒞</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo><mo>→</mo><mi>D</mi><mo>′</mo></mrow><annotation encoding="application/x-tex"> prog \;\colon\; \mathcal{C}(D) \to D' </annotation></semantics></math></div> <p><em>subject to</em> an external <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math>-“<em>context</em>” (<a href="#UustaluVene08">Uustalu & Vene (2008)</a>, <a href="#POM13">POM13</a>)</p> <p>(a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math>-<em>cause</em>).</p> </li> <li> <p>A co-Kleisli co-module for a comonad <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math> is a program</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><msubsup><mi>prvd</mi> <mi>D</mi> <mi>𝒞</mi></msubsup><msub><mi>id</mi> <mi>D</mi></msub><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mi>D</mi><mo>→</mo><mi>𝒞</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex"> prvd^{\mathcal{C}}_D id_D \;\colon\; D \to \mathcal{C}(D) </annotation></semantics></math></div> <p><em>producing</em> or <em>providing</em> such <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>𝒞</mi></mrow><annotation encoding="application/x-tex">\mathcal{C}</annotation></semantics></math>-contexts.</p> <p>(cf. [<a href="#Uustalu21Lecture3">Uustalu (2021), Lect. 3, slide 9</a>])</p> </li> </ul> </li> </ul> <div style="margin: -20px 0px 20px 10px"> <img src="/nlab/files/CoKleisliCompOfContextfulPrograms-230815.jpg" width="800px" /> </div> <p><br /></p> <h3 id="DoNotation">Syntactic idea: Do-notation</h3> <p>Finally, to turn all this into an efficient <a class="existingWikiWord" href="/nlab/show/programming+language">programming language</a> one just has to declare a convenient <a class="existingWikiWord" href="/nlab/show/syntax">syntax</a> for denoting <a class="existingWikiWord" href="/nlab/show/Kleisli+composition">Kleisli composition</a>.</p> <p>One such syntax is known as “<em>do notation</em>” (introduced with “<code>{...}</code>” instead of “<code>do</code>” by <a href="#Launchbury93">Launchbury 1993 §3.3</a>, then promoted by <a class="existingWikiWord" href="/nlab/show/Mark+Jones">Mark Jones</a> in the 1990s [<a href="Haskell#HHPW07">HHPW07, p. 25</a>] and adopted by <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a> in <a href="https://www.haskell.org/definition/from12to13.html#do">version 1.3</a>, for review see <a href="#BentonHughesMoggi02">Benton, Hughes & Moggi 2002 p. 70</a>, <a href="#Milewski19">Milewski 2019 §20.3</a>), which aims to jointly express:</p> <ol> <li> <p>successive Kleisli composition in words like “do this, do that, and return the result”,</p> </li> <li> <p>any intermediate bind-operation as “extracting” a <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>-datum <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>d</mi></mrow><annotation encoding="application/x-tex">d</annotation></semantics></math> out of an <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi><mo stretchy="false">(</mo><mi>D</mi><mo stretchy="false">)</mo></mrow><annotation encoding="application/x-tex">\mathcal{E}(D)</annotation></semantics></math>-datum <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>E</mi></mrow><annotation encoding="application/x-tex">E</annotation></semantics></math> with notation <code>d <- E</code></p> </li> </ol> <p>Syntactically, do-notation is the following <a class="existingWikiWord" href="/nlab/show/syntactic+sugar">syntactic sugar</a> for combined <a class="existingWikiWord" href="/nlab/show/Kleisli+composition">Kleisli composition</a> and <a class="existingWikiWord" href="/nlab/show/bound+variable">variable binding</a>:</p> <ol> <li> <p><code>do prog</code> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>≡</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mrow><annotation encoding="application/x-tex">\;\;\equiv\;\;</annotation></semantics></math> <code>prog</code></p> </li> <li> <p><code>do prog1 prog2</code> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>≡</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mrow><annotation encoding="application/x-tex">\;\;\equiv\;\;</annotation></semantics></math> <code>prog1 bind (\_ -> prog2)</code></p> </li> <li> <p><code>do (x <- prog1) prog2</code> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo>≡</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mrow><annotation encoding="application/x-tex">\;\;\equiv\;\;</annotation></semantics></math> <code>prog1 bind (\x -> prog2)</code></p> </li> </ol> <p>This is, first of all, a suggestive notation (in fact a “<a class="existingWikiWord" href="/nlab/show/domain+specific+embedded+programming+language">domain specific embedded programming language</a>”, see <a href="domain+specific+embedded+programming+language#RelationToMonadicEffects">there</a>) for expressing effect-binding:</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/EffectBindingViaDoNotation-230828.jpg" width="350px" /> </div> <p>but thereby it furthermore provides a convenient means of expressing successive Kleisli-composition simply by successivley “calling” the separate procedures, much in the style of <a class="existingWikiWord" href="/nlab/show/imperative+programming">imperative programming</a> (which thereby is emulated/encapsulated by pure <a class="existingWikiWord" href="/nlab/show/functional+programming">functional programming</a>):</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/KleisliCompositeInDoNotation-230826.jpg" width="520px" /> </div> <p>but the notation becomes more suggestive with the rule that the “<code><-</code>”-symbols may notationally be suppressed for functions with trivial in- or out-put (ie. of <a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo></mrow><annotation encoding="application/x-tex">\ast</annotation></semantics></math>) besides their <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effect, as in this example:</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/PureEffectKleisliCompositeInDoNotation-230826.jpg" width="520px" /> </div> <p>This case brings out clearly how the ambient “<code>do</code>…<code>return</code>”-syntax block expresses the (Kleisli-)composition of any number of <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>ℰ</mi></mrow><annotation encoding="application/x-tex">\mathcal{E}</annotation></semantics></math>-effectful procedures.</p> <p>On top of that the “<code><-</code>”-syntax is meant to be suggestive of <em>reading out</em> a value. This is accurate imagery for the <a class="existingWikiWord" href="/nlab/show/state+monad">state monad</a> (and its abstraction to the <a class="existingWikiWord" href="/nlab/show/IO-monad">IO-monad</a>), where from the two pasic operations of reading/writng a global variable</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>read</mi></mtd> <mtd><mo lspace="verythinmathspace">:</mo></mtd> <mtd><mi>W</mi><mi>State</mi><mo stretchy="false">(</mo><mi>W</mi><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>read</mi></mtd> <mtd><mo>≡</mo></mtd> <mtd><mi>w</mi><mo>↦</mo><mo stretchy="false">(</mo><mi>w</mi><mo>,</mo><mi>w</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mrow><mtable><mtr><mtd><mi>write</mi></mtd> <mtd><mo lspace="verythinmathspace">:</mo></mtd> <mtd><mi>W</mi><mo>→</mo><mi>W</mi><mi>State</mi><mo stretchy="false">(</mo><mo>*</mo><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>write</mi></mtd> <mtd><mo>≡</mo></mtd> <mtd><mi>w</mi><mo>↦</mo><mo stretchy="false">(</mo><mi>w</mi><mo>′</mo><mo>↦</mo><mi>w</mi><mo stretchy="false">)</mo></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ read &\colon& W State(W) \\ read &\equiv& w \mapsto (w,w) } \;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\;\; \array{ write &\colon& W \to W State(\ast) \\ write &\equiv& w \mapsto (w' \mapsto w) } </annotation></semantics></math></div> <p>any <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>-stateful program, such as the simple example</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mi>inc</mi></mtd> <mtd><mo lspace="verythinmathspace">:</mo></mtd> <mtd><mi>ℕ</mi><mi>State</mi><mo stretchy="false">(</mo><mo>*</mo><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mi>inc</mi></mtd> <mtd><mo>≡</mo></mtd> <mtd><mi>n</mi><mo>↦</mo><mi>n</mi><mo>+</mo><mn>1</mn></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ inc &\colon& \mathbb{N}State(\ast) \\ inc &\equiv& n \mapsto n+1 } </annotation></semantics></math></div> <p>may be constucted in do-notation, such as:</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/StatefulNumberIncrementInDONotation-230828.jpg" width="560px" /> </div> <p>For a similar effect monad such as the <a class="existingWikiWord" href="/nlab/show/list+monad">list monad</a> the analogous <code>do</code>-code for incrementing all entries in a list of numbers looks as follows:</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/ListReadKleisliCompositeInDoNotation-230826.jpg" width="520px" /> </div> <p>Here The <code>do</code>-notation on the right evokes the idea that in <em>each step</em> a number <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi><mo lspace="verythinmathspace">:</mo><mi>ℕ</mi></mrow><annotation encoding="application/x-tex">n \colon \mathbb{N}</annotation></semantics></math> is “read out” from MyList and then its increment returned — but leaves linguistically implicit the idea that this operation is to be performed <em>for all elements</em> of the list and all results re-compiled into an output list.</p> <p>Indeed, in general it is misleading to think of Kleisli composition as being about “reading out” data. What Kleisli composition is really about is acting on data that has <em>generators</em> and defining a program by what it does <em>on generators</em>, hence <em>for</em> a given generating datum:</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/KleisliMapsActOnGeneratingData-23-828.jpg" width="560px" /> </div> <p>Therefore the conceptually more accurate (if maybe less concise) program-linguistic reflection of the monadic effect-binding operation would be a “<code>for</code>…<code>do</code>”-block:</p> <div style="margin: -20px 0px 20px 10px"> <img src="/nlab/files/ForDoNotation-230827c.jpg" width="420px" /> </div> <p>In terms of such for-do-notation, the generic case that we started with above has the following syntactic rendering:</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/KleisliCompositeInForDoNotation-230826.jpg" width="670px" /> </div> <p>This syntax may be notationally less concise but it evokes rather closely what is actually going on in programming with monadic effects.</p> <p>For example, the above operation of icrementing all numbers in a given list reads in <code>for</code>…<code>do</code>-notation as follows:</p> <div style="margin: -20px 0px 20px 10px"> <img src="/nlab/files/ListIncrementViaForDo-280827b.jpg" width="750px" /> </div> <p>neatly indicative of how the operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="verythinmathspace" rspace="0em">+</mo><mn>1</mn></mrow><annotation encoding="application/x-tex">+1</annotation></semantics></math> is applied <em>for</em> every number <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>n</mi></mrow><annotation encoding="application/x-tex">n</annotation></semantics></math> found <em>in</em> the list.</p> <p>(NB.: There is no clash with <code>for</code>…<code>do</code>-notation as used for loops in <a class="existingWikiWord" href="/nlab/show/imperative+programming">imperative programming</a>, since <a class="existingWikiWord" href="/nlab/show/functional+programming">functionally</a> these are instead expressed by <a class="existingWikiWord" href="/nlab/show/recursion">recursion</a>.)</p> <p>The appropriateness of rendering effect binding as a <code>for</code>…<code>do</code>-expression becomes yet more pronounced in contexts of <a class="existingWikiWord" href="/nlab/show/substructural+logic">substructural</a> <a class="existingWikiWord" href="/nlab/show/type+theory">typing contexts</a> such as in <a class="existingWikiWord" href="/nlab/show/linear+type+theory">linear type theory</a>, where the idea of “reading out” of monadic types via “<code><-</code>”-notation becomes yet more dubious.</p> <p>For example, consider the <a class="existingWikiWord" href="/nlab/show/relative+monad">relative monad</a> (<a href="relative+monad#LinearSpan">this example</a>) which sends <a class="existingWikiWord" href="/nlab/show/sets">sets</a> to the <a class="existingWikiWord" href="/nlab/show/vector+spaces">vector spaces</a> that are their <a class="existingWikiWord" href="/nlab/show/linear+spans">linear spans</a>:</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mpadded width="0" lspace="-100%width"><mrow><mi mathvariant="normal">Q</mi><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mrow></mpadded><mi>Set</mi></mtd> <mtd><mo>⟶</mo></mtd> <mtd><mi>Vect</mi></mtd></mtr> <mtr><mtd><mi>W</mi></mtd> <mtd><mo>↦</mo></mtd> <mtd><munder><mo>⊕</mo><mi>W</mi></munder><mi>𝟙</mi></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ \mathllap{\mathrm{Q} \;\;\colon\;\;} Set &\longrightarrow& Vect \\ W &\mapsto& \underset{W}{\oplus} \mathbb{1} } </annotation></semantics></math></div> <p>with</p> <div class="maruku-equation"><math xmlns="http://www.w3.org/1998/Math/MathML" display="block" class="maruku-mathml"><semantics><mrow><mrow><mtable><mtr><mtd><mpadded width="0" lspace="-100%width"><mrow><msup><mi>bind</mi> <mi mathvariant="normal">Q</mi></msup><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace><mo lspace="verythinmathspace">:</mo><mspace width="thickmathspace"></mspace><mspace width="thickmathspace"></mspace></mrow></mpadded><mo stretchy="false">(</mo><mi>W</mi><mo>→</mo><mi mathvariant="normal">Q</mi><mi>W</mi><mo>′</mo><mo stretchy="false">)</mo></mtd> <mtd><mo>⟶</mo></mtd> <mtd><mo stretchy="false">(</mo><mi mathvariant="normal">Q</mi><mi>W</mi><mo>→</mo><mi mathvariant="normal">Q</mi><mi>W</mi><mo>′</mo><mo stretchy="false">)</mo></mtd></mtr> <mtr><mtd><mrow><mo>(</mo><mi>w</mi><mo>↦</mo><mrow><mo>|</mo><msub><mi>ψ</mi> <mi>w</mi></msub><mo>⟩</mo></mrow><mo>)</mo></mrow></mtd> <mtd><mo>↦</mo></mtd> <mtd><mrow><mo>(</mo><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mi>w</mi></munder><msub><mi>q</mi> <mrow><msub><mrow></mrow> <mi>W</mi></msub></mrow></msub><mrow><mo>|</mo><mi>w</mi><mo>⟩</mo></mrow><mspace width="thinmathspace"></mspace><mo>↦</mo><mspace width="thinmathspace"></mspace><munder><mo lspace="thinmathspace" rspace="thinmathspace">∑</mo> <mi>w</mi></munder><msub><mi>q</mi> <mrow><msub><mrow></mrow> <mi>w</mi></msub></mrow></msub><mrow><mo>|</mo><msub><mi>ψ</mi> <mi>w</mi></msub><mo>⟩</mo></mrow><mo>)</mo></mrow></mtd></mtr></mtable></mrow></mrow><annotation encoding="application/x-tex"> \array{ \mathllap{bind^{\mathrm{Q}} \;\;\colon\;\;} (W \to \mathrm{Q}W') &\longrightarrow& (\mathrm{Q}W \to \mathrm{Q}W') \\ \left( w \mapsto \left\vert \psi_w \right\rangle \right) &\mapsto& \left( \sum_w q_{{}_W} \left\vert w \right\rangle \,\mapsto\, \sum_w q_{{}_w} \left\vert \psi_w \right\rangle \right) } </annotation></semantics></math></div> <p>In this case the traditional <code>do</code>-notation would suggest that given a vector one may “read out” a basis element from it – which does not make conceptual sense.</p> <p>Instead, what’s really happening is that to define a linear map <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>G</mi><mo lspace="verythinmathspace">:</mo><mi mathvariant="normal">Q</mi><mi>W</mi><mo>→</mo><mi class="mathscript">ℋ</mi></mrow><annotation encoding="application/x-tex">G \colon \mathrm{Q}W \to \mathscr{H}</annotation></semantics></math> on a vector space equipped with a <a class="existingWikiWord" href="/nlab/show/basis+of+a+vector+space">linear basis</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math> (literally: a set of free <a href="basis+of+a+vector+space#GeneratedVectorSpace">generators</a>) it is sufficient to define this map <em>for</em> each basis-vector <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mrow><mo>|</mo><mi>w</mi><mo>⟩</mo></mrow></mrow><annotation encoding="application/x-tex">\left\vert w \right\rangle</annotation></semantics></math> — and this is just what the <code>for</code>…<code>do</code>-notation for the <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi mathvariant="normal">Q</mi></mrow><annotation encoding="application/x-tex">\mathrm{Q}</annotation></semantics></math>-monad expresses:</p> <div style="margin: -30px 0px 20px 10px"> <img src="/nlab/files/LinearMapInForDoNotation-230828.jpg" width="150px" /> </div> <p><br /></p> <h2 id="Examples">Examples</h2> <h3 id="definable_monads">Definable monads</h3> <p>Various monads are <em>definable</em> in terms of standard <a class="existingWikiWord" href="/nlab/show/type+formation">type-forming operations</a> (such as <a class="existingWikiWord" href="/nlab/show/product+types">product types</a>, <a class="existingWikiWord" href="/nlab/show/function+types">function types</a>, etc.). These include the following (cf. <a href="#Moggi91">Moggi 1991, Exp. 1.1</a>):</p> <ul> <li> <p>The <em><a class="existingWikiWord" href="/nlab/show/maybe+monad">maybe monad</a></em> encodes possible controlled failure of a program to execute.</p> </li> <li> <p>An <em><a class="existingWikiWord" href="/nlab/show/exception+monad">exception monad</a></em>, more generally, encodes possible controlled failure together with the output of an error “message” in the general form of data of some type.</p> </li> <li> <p>The <em><a class="existingWikiWord" href="/nlab/show/reader+monad">reader monad</a></em> and <em><a class="existingWikiWord" href="/nlab/show/coreader+comonad">coreader comonad</a></em> both encode reading out a global parameter.</p> </li> <li> <p>The <em><a class="existingWikiWord" href="/nlab/show/writer+monad">writer monad</a></em> and <em><a class="existingWikiWord" href="/nlab/show/cowriter+comonad">cowriter comonad</a></em> both encode writing <em>consecutively</em> into a global resource, such as for a <a class="existingWikiWord" href="/nlab/show/stream">stream</a>.</p> </li> <li> <p>The <em><a class="existingWikiWord" href="/nlab/show/state+monad">state monad</a></em> encodes the possibility of <em>consecutive reading and re-setting</em> a global parameter – this provides a notion of <em><a class="existingWikiWord" href="/nlab/show/random+access+memory">random access memory</a></em>.</p> </li> <li> <p>The <em><a class="existingWikiWord" href="/nlab/show/costate+comonad">costate comonad</a></em> encodes a way (a “<a class="existingWikiWord" href="/nlab/show/lens+in+computer+science">lens</a>”) to read and write fields in <a class="existingWikiWord" href="/nlab/show/databases">databases</a>.</p> </li> <li> <p>The <em><a class="existingWikiWord" href="/nlab/show/continuation+monad">continuation monad</a></em> encodes <a class="existingWikiWord" href="/nlab/show/continuation-passing+style">continuation-passing style</a> of program execution.</p> </li> <li> <p>The <em><a class="existingWikiWord" href="/nlab/show/selection+monad">selection monad</a></em> encodes selecting a value of a type depending on the values of some function on it.</p> </li> </ul> <h4 id="StateMonad">State monad and Random access memory</h4> <p>A <a class="existingWikiWord" href="/nlab/show/functional+program">functional program</a> with input of <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi></mrow><annotation encoding="application/x-tex">D</annotation></semantics></math>, output of <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>′</mo></mrow><annotation encoding="application/x-tex">D'</annotation></semantics></math> and <em>mutable state <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math></em> is a <a class="existingWikiWord" href="/nlab/show/function">function</a> (<a class="existingWikiWord" href="/nlab/show/morphism">morphism</a>) of <a class="existingWikiWord" href="/nlab/show/type">type</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>×</mo><mi>W</mi><mo>⟶</mo><mi>D</mi><mo>′</mo><mo>×</mo><mi>W</mi></mrow><annotation encoding="application/x-tex">D \times W \longrightarrow D' \times W</annotation></semantics></math> – also called a <em><a class="existingWikiWord" href="/nlab/show/Mealy+machine">Mealy machine</a></em> (see <a href="Mealy+machine#MealyMachinesAsEffectfulMaps">there</a>).</p> <p>Under the (<a class="existingWikiWord" href="/nlab/show/Cartesian+product">Cartesian product</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>⊣</mo></mrow><annotation encoding="application/x-tex">\dashv</annotation></semantics></math> <a class="existingWikiWord" href="/nlab/show/internal+hom">internal hom</a>)-<a class="existingWikiWord" href="/nlab/show/adjunction">adjunction</a> (<a class="existingWikiWord" href="/nlab/show/currying">currying</a>) this is equivalently given by its <a class="existingWikiWord" href="/nlab/show/adjunct">adjunct</a>, which is a function of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>D</mi><mo>⟶</mo><mo stretchy="false">[</mo><mi>W</mi><mo>,</mo><mi>W</mi><mo>×</mo><mi>D</mi><mo>′</mo><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">D \longrightarrow [W, W \times D' ]</annotation></semantics></math>. Here the operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>W</mi><mo>,</mo><mi>W</mi><mo>×</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[W, W\times (-)]</annotation></semantics></math> is the <a class="existingWikiWord" href="/nlab/show/monad">monad</a> induced by the above adjunction and this latter function is naturally regarded as a morphism in the <a class="existingWikiWord" href="/nlab/show/Kleisli+category">Kleisli category</a> of this monad. This monad <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo stretchy="false">[</mo><mi>W</mi><mo>,</mo><mi>W</mi><mo>×</mo><mo stretchy="false">(</mo><mo lspace="verythinmathspace" rspace="0em">−</mo><mo stretchy="false">)</mo><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">[W, W\times (-)]</annotation></semantics></math> is called the <em><a class="existingWikiWord" href="/nlab/show/state+monad">state monad</a></em> for mutable states of type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>W</mi></mrow><annotation encoding="application/x-tex">W</annotation></semantics></math>:</p> <center> <img src="/nlab/files/State-Effectful-Program-230804.jpg" width="600" /> </center> <h4 id="maybe_monad_and_controlled_failure">Maybe monad and Controlled failure</h4> <p>The <strong><a class="existingWikiWord" href="/nlab/show/maybe+monad">maybe monad</a></strong> is the operation <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↦</mo><mi>X</mi><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo><mo>*</mo></mrow><annotation encoding="application/x-tex">X \mapsto X \coprod \ast</annotation></semantics></math>. The idea here is that a function <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>⟶</mo><mi>Y</mi></mrow><annotation encoding="application/x-tex">X \longrightarrow Y</annotation></semantics></math> in its <a class="existingWikiWord" href="/nlab/show/Kleisli+category">Kleisli category</a> is in the original category a function of the form <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>⟶</mo><mi>Y</mi><mo lspace="thinmathspace" rspace="thinmathspace">∐</mo><mo>*</mo></mrow><annotation encoding="application/x-tex">X \longrightarrow Y \coprod \ast </annotation></semantics></math> so either returns indeed a value in <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Y</mi></mrow><annotation encoding="application/x-tex">Y</annotation></semantics></math> or else returns the unique element of the <a class="existingWikiWord" href="/nlab/show/unit+type">unit type</a>/<a class="existingWikiWord" href="/nlab/show/terminal+object">terminal object</a> <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>*</mo></mrow><annotation encoding="application/x-tex">\ast</annotation></semantics></math>. This is then naturally interpreted as “no value returned”, hence as indicating a “failure in computation”.</p> <h4 id="exception_monad_and_exception_handling">Exception monad and Exception handling</h4> <p>(…) <a class="existingWikiWord" href="/nlab/show/exception+monad">exception monad</a> (…)</p> <h4 id="continuation_monad_and_continuationpassing">Continuation monad and Continuation-passing</h4> <p>The <a class="existingWikiWord" href="/nlab/show/continuation+monad">continuation monad</a> on a given type <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>S</mi></mrow><annotation encoding="application/x-tex">S</annotation></semantics></math> acts by <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>X</mi><mo>↦</mo><mo stretchy="false">[</mo><mo stretchy="false">[</mo><mi>X</mi><mo>,</mo><mi>S</mi><mo stretchy="false">]</mo><mo>,</mo><mi>S</mi><mo stretchy="false">]</mo></mrow><annotation encoding="application/x-tex">X \mapsto [[X,S],S]</annotation></semantics></math>.</p> <p>(…)</p> <h3 id="axiomatic_monads">Axiomatic monads</h3> <p>Other monads may be supplied “axiomatically” by the programming language, meaning that they are data structures <a class="existingWikiWord" href="/nlab/show/type">typed</a> as monads, but whose actual type formation, binding- and return-operations are special purpose operations provided by the programming environment.</p> <p>This includes:</p> <ul> <li> <p>the <em><a class="existingWikiWord" href="/nlab/show/IO+monad">IO monad</a></em> in <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a>,</p> </li> <li> <p>the <em><a class="existingWikiWord" href="/nlab/show/completion+monad">completion monad</a></em>, as in <a class="existingWikiWord" href="/nlab/show/constructive+analysis">constructive analysis</a>, used for dealing for instance with <a class="existingWikiWord" href="/nlab/show/real+numbers">real numbers</a>.</p> </li> </ul> <p>In this vein:</p> <ul> <li>Equipping <a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy type theory</a> (say implemented as a programming language concretely in <a class="existingWikiWord" href="/nlab/show/Coq">Coq</a> or <a class="existingWikiWord" href="/nlab/show/Agda">Agda</a>) with two axiomatic <a class="existingWikiWord" href="/nlab/show/idempotent+monads">idempotent monads</a>, denoted <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>♯</mo></mrow><annotation encoding="application/x-tex">\sharp</annotation></semantics></math> and <math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mi>Π</mi></mrow><annotation encoding="application/x-tex">\Pi</annotation></semantics></math>, with some additional data and relations, turns it into <em><a class="existingWikiWord" href="/nlab/show/cohesive+homotopy+type+theory">cohesive homotopy type theory</a></em>. See also at <em><a href="Agda#AgdaFlat">Agda flat</a></em> and at <em><a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a></em>.</li> </ul> <h2 id="related_concepts">Related concepts</h2> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/extension+system">extension system</a></p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/relative+monad">relative monad</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/polymonad">polymonad</a></p> </li> </ul> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/relation+between+type+theory+and+category+theory">relation between type theory and category theory</a>, <a class="existingWikiWord" href="/nlab/show/categorical+semantics">categorical semantics</a>, <a class="existingWikiWord" href="/nlab/show/categorical+logic">categorical logic</a></p> </li> <li> <p>Examples of (co)monads in (<a class="existingWikiWord" href="/nlab/show/homotopy+type+theory">homotopy</a>) <a class="existingWikiWord" href="/nlab/show/type+theory">type theory</a> involve in particular <em><a class="existingWikiWord" href="/nlab/show/modal+operators">modal operators</a></em> as they appear in</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/modal+logic">modal logic</a>/<a class="existingWikiWord" href="/nlab/show/modal+type+theory">modal type theory</a>/<a class="existingWikiWord" href="/nlab/show/computational+type+theory">computational type theory</a>.</li> </ul> <p>See also:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/adjoint+modality">adjoint modality</a>.</li> </ul> </li> <li> <p>For an approach to composing monads, see</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/monad+transformer">monad transformer</a></li> </ul> </li> <li> <p>Another approach to modelling side effects in <a class="existingWikiWord" href="/nlab/show/functional+programming+languages">functional programming languages</a> are</p> <p><a class="existingWikiWord" href="/nlab/show/algebraic+side+effects">algebraic side effects</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/free+monad">Free monads</a> in computer science appear in the concepts of</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/initial+algebra+for+an+endofunctor">initial algebra for an endofunctor</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/terminal+coalgebra+for+an+endofunctor">terminal coalgebra for an endofunctor</a></p> </li> </ul> </li> <li> <p>Other generalizations are:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/arrow+%28in+computer+science%29">arrow (in computer science)</a></p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/applicative+functor">applicative functor</a></p> </li> </ul> </li> <li> <p>There is also: <a class="existingWikiWord" href="/nlab/show/monad+%28in+linguistics%29">monad (in linguistics)</a></p> </li> </ul> <h2 id="references">References</h2> <h3 id="ReferencesGeneral">General</h3> <p>The <a class="existingWikiWord" href="/nlab/show/extension+system">extension system</a>-style presentation of monads as used in computer science is briefly mentioned in:</p> <ul> <li id="Manes76"><a class="existingWikiWord" href="/nlab/show/Ernest+G.+Manes">Ernest G. Manes</a>, Sec 3, Ex. 12 (p. 32) of: <em>Algebraic Theories</em>, Springer (1976) [<a href="https://doi.org/10.1007/978-1-4612-9860-1">doi:10.1007/978-1-4612-9860-1</a>]</li> </ul> <p>and expanded on in</p> <ul> <li id="MarmolejoWood10"><a class="existingWikiWord" href="/nlab/show/Francisco+Marmolejo">Francisco Marmolejo</a>, <a class="existingWikiWord" href="/nlab/show/Richard+J.+Wood">Richard J. Wood</a>, <em>Monads as extension systems – no iteration is necessary</em>, <a class="existingWikiWord" href="/nlab/show/TAC">TAC</a> <strong>24</strong> 4 (2010) 84-113 [<a href="http://www.tac.mta.ca/tac/volumes/24/4/24-04abs.html">tac:24-04</a>]</li> </ul> <p>but not related there to computation.</p> <p>The original observation of monads as “notions of computation” is:</p> <ul> <li id="Moggi89"> <p><a class="existingWikiWord" href="/nlab/show/Eugenio+Moggi">Eugenio Moggi</a>, <em>Computational lambda-calculus and monads</em>, in: <em>Proceedings of the Fourth Annual Symposium on Logic in Computer Science</em> (1989) 14-23 [<a href="https://doi.org/10.1109/LICS.1989.39155">doi:10.1109/LICS.1989.39155</a>]</p> </li> <li id="Moggi89Abstract"> <p><a class="existingWikiWord" href="/nlab/show/Eugenio+Moggi">Eugenio Moggi</a>, <em>An abstract View of Programming Languages</em>, LFCS report ECS-LFCS-90-113 (1989) [<a href="http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-113">web</a>, <a class="existingWikiWord" href="/nlab/files/Moggi-AbstractView.pdf" title="pdf">pdf</a>]</p> <blockquote> <p>(considers also <a href="monad#BicategoryOfMonads">transformations of monads</a> in Def. 4.0.8)</p> </blockquote> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Philip+Wadler">Philip Wadler</a>, <em>Comprehending Monads</em>, in <em>Conference on Lisp and functional programming</em>, ACM Press (1990) [<a class="existingWikiWord" href="/nlab/files/WadlerMonads.pdf" title="pdf">pdf</a>, <a href="https://doi.org/10.1145/91556.91592">doi:10.1145/91556.91592</a>]</p> </li> <li id="Moggi91"> <p><a class="existingWikiWord" href="/nlab/show/Eugenio+Moggi">Eugenio Moggi</a>, <em>Notions of computation and monads</em>, Information and Computation, <strong>93</strong> 1 (1991) [<a href="https://doi.org/10.1016/0890-5401(91)90052-4">doi:10.1016/0890-5401(91)90052-4</a>, <a href="http://www.disi.unige.it/person/MoggiE/ftp/ic91.pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Philip+Wadler">Philip Wadler</a>, <em>The essence of functional programming</em>, <em>POPL ‘92: Principles of programming languages</em> (1992) 1-14 [<a href="https://doi.org/10.1145/143165.143169">doi:10.1145/143165.143169</a>, <a href="https://jgbm.github.io/eecs762f19/papers/wadler-monads.pdf">pdf</a>]</p> </li> </ul> <p>Further discussion:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Gordon+Plotkin">Gordon Plotkin</a>, <a class="existingWikiWord" href="/nlab/show/John+Power">John Power</a>, <em>Notions of Computation Determine Monads</em>, in: <em>Foundations of Software Science and Computation Structures</em> FoSSaCS 2002, Lecture Notes in Computer Science <strong>2303</strong>, Springer (2002) [<a href="https://doi.org/10.1007/3-540-45931-6_24">doi:10.1007/3-540-45931-6_24</a>, <a href="https://era.ed.ac.uk/handle/1842/196">era:1842/196</a>]</li> </ul> <p>On the impact of <a href="#Moggi91">Moggi (1991)</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Martin+Hyland">Martin Hyland</a>, <a class="existingWikiWord" href="/nlab/show/John+Power">John Power</a>, §6 of: <em>The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads</em>, Electronic Notes in Theor. Comp. Sci. <strong>172</strong> (2007) 437-458 [<a href="https://doi.org/10.1016/j.entcs.2007.02.019">doi:10.1016/j.entcs.2007.02.019</a>, <a href="https://www.dpmms.cam.ac.uk/~jmeh1/Research/Publications/2007/hp07.pdf">preprint</a>]</li> </ul> <p>Origin of the <a class="existingWikiWord" href="/nlab/show/do-notation">do-notation</a> for <a class="existingWikiWord" href="/nlab/show/Kleisli+composition">Kleisli composition</a> of effectful programs:</p> <ul> <li id="Launchbury93"><a class="existingWikiWord" href="/nlab/show/John+Launchbury">John Launchbury</a>, §3.3 in: <em>Lazy imperative programming</em>, Proceedings of <em>ACM Sigplan Workshop on State in Programming Languages</em>, Copenhagen (1993) [<a href="https://launchbury.files.wordpress.com/2019/01/lazy-imperative-programming.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Launchbury-LazyImperative.pdf" title="pdf">pdf</a>]</li> </ul> <p>Introducing the notion of <a class="existingWikiWord" href="/nlab/show/monad+transformers">monad transformers</a>:</p> <ul> <li id="Espinosa94"> <p><a class="existingWikiWord" href="/nlab/show/David+A.+Espinosa">David A. Espinosa</a>, §3.2 in: <em>Building Interpreters by Transforming Stratified Monads</em> (1994) [<a href="https://github.com/davidespinosa01/papers/blob/master/E/Espinosa%20David/espinosa-stratified-monads.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Espinosa-StratifiedMonads.pdf" title="pdf">pdf</a>]</p> </li> <li id="Espinosa95"> <p><a class="existingWikiWord" href="/nlab/show/David+A.+Espinosa">David A. Espinosa</a>, §2.6 in: <em>Semantic Lego</em>, PhD thesis, Columbia University (1995) [<a href="https://github.com/davidespinosa01/papers/blob/master/E/Espinosa%20David/espinosa-stratified-monads.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Espinosa-SemanticLego.pdf" title="pdf">pdf</a>, slides:<a href="https://github.com/davidespinosa01/papers/blob/346c2ded6af78805701106d51daee8f7a756c948/E/Espinosa%20David/espinosa-thesis-slides.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Espinosa-SemanticLego-slides.pdf" title="pdf">pdf</a>]</p> </li> <li id="LiangHudakJones95"> <p>Sheng Liang, <a class="existingWikiWord" href="/nlab/show/Paul+Hudak">Paul Hudak</a>, <a class="existingWikiWord" href="/nlab/show/Mark+Jones">Mark Jones</a>, <em>Monad transformers and modular interpreters</em>, POPL ‘95 (1995) 333–343 [<a href="https://doi.org/10.1145/199448.199528">doi:10.1145/199448.199528</a>]</p> </li> </ul> <p>More (early) literature is listed here:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/David+A.+Espinosa">David A. Espinosa</a>, <em><a href="https://github.com/davidespinosa01/effects-bibliography">Effects bibliography</a></em></li> </ul> <p>In the generality of <a class="existingWikiWord" href="/nlab/show/relative+monads">relative monads</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Thorsten+Altenkirch">Thorsten Altenkirch</a>, <a class="existingWikiWord" href="/nlab/show/James+Chapman">James Chapman</a>, <a class="existingWikiWord" href="/nlab/show/Tarmo+Uustalu">Tarmo Uustalu</a>, Section 2 of: <em>Monads need not be endofunctors</em>, Logical Methods in Computer Science <strong>11</strong> 1:3 (2015) 1–40 [<a href="https://arxiv.org/abs/1412.7148">arXiv:1412.7148</a>, <a href="http://www.cs.nott.ac.uk/~txa/publ/jrelmon.pdf">pdf</a>, <a href="https://doi.org/10.2168/LMCS-11(1:3)2015">doi:10.2168/LMCS-11(1:3)2015</a>]</li> </ul> <p>The dual notion of <a class="existingWikiWord" href="/nlab/show/comonads+in+computer+science">comonads in computer science</a> as modelling <em>contexts</em>:</p> <ul> <li id="UustaluVene08"> <p><a class="existingWikiWord" href="/nlab/show/Tarmo+Uustalu">Tarmo Uustalu</a>, <a class="existingWikiWord" href="/nlab/show/Varmo+Vene">Varmo Vene</a>, <em>Comonadic Notions of Computation</em>, Electronic Notes in Theoretical Computer Science <strong>203</strong> 5 (2008) 263-284 [<a href="https://doi.org/10.1016/j.entcs.2008.05.029">doi:10.1016/j.entcs.2008.05.029</a>]</p> </li> <li id="POM13"> <p><a class="existingWikiWord" href="/nlab/show/Tomas+Petricek">Tomas Petricek</a>, <a class="existingWikiWord" href="/nlab/show/Dominic+Orchard">Dominic Orchard</a>, <a class="existingWikiWord" href="/nlab/show/Alan+Mycroft">Alan Mycroft</a>, <em>Coeffects: Unified Static Analysis of Context-Dependence</em>, in: <em>Automata, Languages, and Programming. ICALP 2013</em>, Lecture Notes in Computer Science <strong>7966</strong> Springer (2013) [<a href="https://doi.org/10.1007/978-3-642-39212-2_35">doi:10.1007/978-3-642-39212-2_35</a>]</p> </li> <li id="Overton14"> <p>David Overton, <em>Comonads in Haskell</em> (2014) [<a href="https://speakerdeck.com/dmoverton/comonads-in-haskell">web</a>, <a class="existingWikiWord" href="/nlab/files/Overton-ComonadsHaskell.pdf" title="pdf">pdf</a>]</p> <blockquote> <p>(in <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a>)</p> </blockquote> </li> </ul> <p>on codo-notation for comonadic contexts:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Dominic+Orchard">Dominic Orchard</a>, <a class="existingWikiWord" href="/nlab/show/Alan+Mycroft">Alan Mycroft</a>, <em>A Notation for Comonads</em>, in: <em>Implementation and Application of Functional Languages. IFL 2012</em>, Lecture Notes in Computer Science <strong>8241</strong> [<a href="https://doi.org/10.1007/978-3-642-41582-1_1">doi:10.1007/978-3-642-41582-1_1</a>]</li> </ul> <p>and emphasis on the combination of <a class="existingWikiWord" href="/nlab/show/monads">monads</a>, <a class="existingWikiWord" href="/nlab/show/comonads">comonads</a> and <a class="existingWikiWord" href="/nlab/show/graded+modalities">graded modalities</a>:</p> <ul> <li id="GKOBU16"> <p>Marco Gaboardi, <a class="existingWikiWord" href="/nlab/show/Shin-ya+Katsumata">Shin-ya Katsumata</a>, <a class="existingWikiWord" href="/nlab/show/Dominic+Orchard">Dominic Orchard</a>, Flavien Breuvart, <a class="existingWikiWord" href="/nlab/show/Tarmo+Uustalu">Tarmo Uustalu</a>, <em>Combining effects and coeffects via grading</em>, ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (2016) 476–489 [<a href="https://doi.org/10.1145/2951913.2951939">doi:10.1145/2951913.2951939</a>, <a href="https://icfp16.sigplan.org/details/icfp-2016-papers/31/Combining-Effects-and-Coeffects-via-Grading">talk abstract</a>, <a href="https://www.youtube.com/watch?v=l1ZNMT3fQCo">video rec</a>]</p> </li> <li id="KRU20"> <p><a class="existingWikiWord" href="/nlab/show/Shin-ya+Katsumata">Shin-ya Katsumata</a>, Exequiel Rivas, <a class="existingWikiWord" href="/nlab/show/Tarmo+Uustalu">Tarmo Uustalu</a>, LICS (2020) 604-618 <em>Interaction laws of monads and comonads</em> [<a href="https://arxiv.org/abs/1912.13477">arXiv:1912.13477</a>, <a href="https://doi.org/10.1145/3373718.3394808">doi:10.1145/3373718.3394808</a>]</p> </li> </ul> <p>The identification of (co)effect handling with (<a class="existingWikiWord" href="/nlab/show/comodule+over+a+comonad">co</a>)<a class="existingWikiWord" href="/nlab/show/modules+over+a+monad">modales</a> over the given (co)monad:</p> <ul> <li> <p><a class="existingWikiWord" href="/nlab/show/Gordon+D.+Plotkin">Gordon D. Plotkin</a>, <a class="existingWikiWord" href="/nlab/show/Matija+Pretnar">Matija Pretnar</a>, <em>Handling Algebraic Effects</em>, Logical Methods in Computer Science, <strong>9</strong> 4 (2013) lmcs:705 [<a href="https://arxiv.org/abs/1312.1399">arXiv:1312.1399</a>, <a href=" https://doi.org/10.2168/LMCS-9(4:23)2013">doi:10.2168/LMCS-9(4:23)2013</a>]</p> </li> <li> <p>Ohad Kammar, Sam Lindley, Nicolas Oury, <em>Handlers in action</em>, ACM SIGPLAN Notices <strong>48</strong> 9 (2013) 145–158 [<a href="https://doi.org/10.1145/2544174.2500590">doi:10.1145/2544174.2500590</a>]</p> </li> </ul> <p id="ReferencesInActualPorgrammingLanguages"> Discussion in actual <a class="existingWikiWord" href="/nlab/show/programming+languages">programming languages</a> such as <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a>:</p> <ul> <li id="BentonHughesMoggi02"> <p><a class="existingWikiWord" href="/nlab/show/Nick+Benton">Nick Benton</a>, <a class="existingWikiWord" href="/nlab/show/John+Hughes">John Hughes</a>, <a class="existingWikiWord" href="/nlab/show/Eugenio+Moggi">Eugenio Moggi</a>, <em>Monads and Effects</em>, in: <em>Applied Semantics</em>, Lecture Notes in Computer Science <strong>2395</strong>, Springer (2002) 42-122 [<a href="https://doi.org/10.1007/3-540-45699-6_2">doi:10.1007/3-540-45699-6_2</a>]</p> </li> <li id="Milewski19"> <p><a class="existingWikiWord" href="/nlab/show/Bartosz+Milewski">Bartosz Milewski</a> (compiled by Igal Tabachnik), “Monads: Programmer’s Definition”, §20 in: <em>Category Theory for Programmers</em>, Blurb (2019) [<a href="https://github.com/hmemcpy/milewski-ctfp-pdf/releases/download/v1.3.0/category-theory-for-programmers.pdf">pdf</a>, <a href="https://github.com/hmemcpy/milewski-ctfp-pdf">github</a>, <a href="https://bartoszmilewski.com/2014/10/28/category-theory-for-programmers-the-preface/">webpage</a>, <a href="https://www.blurb.com/b/9621951-category-theory-for-programmers-new-edition-hardco">ISBN:9780464243878</a>]</p> </li> <li id="Milewski23"> <p><a class="existingWikiWord" href="/nlab/show/Bartosz+Milewski">Bartosz Milewski</a>, §14 in: <em>The Dao of Functional Programming</em> (2023) [<a href="https://github.com/BartoszMilewski/Publications/blob/master/TheDaoOfFP/DaoFP.pdf">pdf</a>, <a href="https://github.com/BartoszMilewski/Publications/tree/master/TheDaoOfFP">github</a>]</p> </li> </ul> <p>and <a class="existingWikiWord" href="/nlab/show/Scala">Scala</a>:</p> <ul> <li id="Winitzki22"><a class="existingWikiWord" href="/nlab/show/Sergei+Winitzki">Sergei Winitzki</a>, Section 10 of: <em>The Science of Functional Programming – A tutorial, with examples in Scala</em> (2022) [<a href="https://leanpub.com/sofp">leanpub:sofp</a>, <a href="https://github.com/winitzki/sofp">github:sofp</a>]</li> </ul> <p>Further discussion/exposition of the notion and application of (co)monads in computer science:</p> <ul> <li id="BrookesGeva91"> <p><a class="existingWikiWord" href="/nlab/show/Stephen+Brookes">Stephen Brookes</a>, Shai Geva, <em>Computational Comonads and Intensional Semantics</em>, CMU-CS-91-190 (1991) [<a class="existingWikiWord" href="/nlab/files/BrookersGeva-ComputationalComonads.pdf" title="pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Philip+Wadler">Philip Wadler</a>, <em>Monads for functional programming</em>, in M. Broy (eds.) <em>Program Design Calculi</em> NATO ASI Series, <strong>118</strong> Springer (1992) [<a href="https://doi.org/10.1007/978-3-662-02880-3_8">doi;10.1007/978-3-662-02880-3_8</a>, <a href="https://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf">pdf</a>]</p> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/Philip+S.+Mulry">Philip S. Mulry</a>: <em>Monads in semantics</em>, Electronic Notes in Theoretical Computer Science <strong>14</strong> (1998) 275-286 [<a href="https://doi.org/10.1016/S1571-0661(05)80241-5">doi:10.1016/S1571-0661(05)80241-5</a>]</p> </li> <li id="BrookesVanStone93"> <p><a class="existingWikiWord" href="/nlab/show/Stephen+Brookes">Stephen Brookes</a>, <a class="existingWikiWord" href="/nlab/show/Kathryn+Van+Stone">Kathryn Van Stone</a>, <em>Monads and Comonads in Intensional Semantics</em> (1993) [<a href="https://apps.dtic.mil/sti/citations/ADA266522">dtic:ADA266522</a>, <a href="https://www.cs.cmu.edu/~brookes/papers/MonadsComonads.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/BrookesVanStone-CoMonads.pdf" title="pdf">pdf</a>]</p> <blockquote> <p>(with <a class="existingWikiWord" href="/nlab/show/distributive+law">distributive law</a> of comonad over monad)</p> </blockquote> </li> <li> <p><a class="existingWikiWord" href="/nlab/show/John+Hughes">John Hughes</a>, section 2 of: <em>Generalising Monads to Arrows</em>, Science of Computer Programming (Elsevier) 37 (1-3): 67–111. (2000) (<a href="http://pdn.sciencedirect.com/science?_ob=MiamiImageURL&_cid=271600&_user=10&_pii=S0167642399000234&_check=y&_origin=search&_zone=rslt_list_item&_coverDate=2000-05-31&wchp=dGLzVlk-zSkWb&md5=fa91ab4ffc136b0cedc52318c7c249be&pid=1-s2.0-S0167642399000234-main.pdf">pdf</a>)</p> </li> <li id="Harper"> <p><a class="existingWikiWord" href="/nlab/show/Robert+Harper">Robert Harper</a>, <em>Of course ML Has Monads!</em> (2011) (<a href="http://existentialtype.wordpress.com/2011/05/01/of-course-ml-has-monads/">web</a>)</p> </li> <li id="Benton15"> <p><a class="existingWikiWord" href="/nlab/show/Nick+Benton">Nick Benton</a>, <em>Categorical Monads and Computer Programming</em>, in: <em><a href="https://www.lms.ac.uk/2015/impact150-stories-impact-mathematics">Impact150: stories of the impact of mathematics</a></em>. London Mathematical Society (2015) [<a href="https://www.lms.ac.uk/sites/lms.ac.uk/files/2.%20Benton%20-%20Categorical%20Monads%20and%20Computer%20Programming.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Benton-CategoricalMonads.pdf" title="pdf">pdf</a>, <a href="https://www.lms.ac.uk/2015/impact150-stories-impact-mathematics">doi:10.1112/i150lms/t.0002</a>]</p> </li> <li id="Riehl17"> <p><a class="existingWikiWord" href="/nlab/show/Emily+Riehl">Emily Riehl</a>, <em>A categorical view of computational effects</em>, talk at <em><a href="https://www.composeconference.org/2017/">C<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∘</mo></mrow><annotation encoding="application/x-tex">\circ</annotation></semantics></math>mp<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo>∘</mo></mrow><annotation encoding="application/x-tex">\circ</annotation></semantics></math>se<math xmlns="http://www.w3.org/1998/Math/MathML" display="inline" class="maruku-mathml"><semantics><mrow><mo lspace="verythinmathspace">:</mo><mspace width="negativethinmathspace"></mspace><mo lspace="verythinmathspace">:</mo></mrow><annotation encoding="application/x-tex">\colon\!\colon</annotation></semantics></math>Conference</a></em> (2017) [<a href="http://www.math.jhu.edu/~eriehl/compose.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Riehl-ComputationalEffects.pdf" title="pdf">pdf</a>]</p> </li> <li> <p>Rob Norris, <em>Functional Programming with Effects</em>, talk at <em>Scala Days 2018</em> [video: <a href="https://youtu.be/30q6BkBv5MY">YT</a>]</p> </li> <li id="Uustalu21"> <p><a class="existingWikiWord" href="/nlab/show/Tarmo+Uustalu">Tarmo Uustalu</a>, lecture notes for <a href="https://staffwww.dcs.shef.ac.uk/people/G.Struth/mgs21.html">MGS 2021</a> (2021):</p> <p id="Uustalu21Lecture1"> <em>Monads and Interaction Lecture 1</em> [<a href="https://cs.ioc.ee/~tarmo/mgs21/mgs1.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Uustalu-Monads1.pdf" title="pdf">pdf</a>]</p> <p id="Uustalu21Lecture2"> <em>Monads and Interaction Lecture 2</em> [<a href="https://cs.ioc.ee/~tarmo/mgs21/mgs2.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Uustalu-Monads2.pdf" title="pdf">pdf</a>]</p> <p id="Uustalu21Lecture3"> <em>Monads and Interaction Lecture 3</em> [<a href="https://cs.ioc.ee/~tarmo/mgs21/mgs3.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Uustalu-Monads3.pdf" title="pdf">pdf</a>]</p> <p id="Uustalu21Lecture4"> <em>Monads and Interaction Lecture 4</em> [<a href="https://cs.ioc.ee/~tarmo/mgs21/mgs4.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Uustalu-Monads4.pdf" title="pdf">pdf</a>]</p> </li> <li> <p>Christina Kohl, Christina Schwaiger, <em>Monads in Computer Science</em> (2021) [<a href="https://www.uibk.ac.at/mathematik/algebra/staff/fritz-tobias/ct2021_course_projects/category_theory.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/KohlSchwaiger-Monads.pdf" title="pdf">pdf</a>]</p> </li> </ul> <p>See also:</p> <ul> <li> <p>Wikipedia, <em><a href="https://en.wikipedia.org/wiki/Monad_(functional_programming)">Monad (functional programming)</a></em></p> </li> <li> <p>Wikipedia, <em><a href="https://en.wikipedia.org/wiki/Side_effect_(computer_science)">Side_effect_(computer_science)</a></em></p> </li> </ul> <p>The specification of <a class="existingWikiWord" href="/nlab/show/monads">monads</a> in <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a> is at:</p> <ul> <li> <p><a href="http://www.haskell.org/haskellwiki/Haskell">The Haskell programming language</a>,</p> <ul> <li> <p><em><a href="https://wiki.haskell.org/Monad">Monad</a></em></p> </li> <li> <p><em><a href="http://www.haskell.org/haskellwiki/Monad_laws">Monad laws</a></em></p> </li> </ul> </li> </ul> <p>and an exposition of <a class="existingWikiWord" href="/nlab/show/category+theory">category theory</a> and monads in terms of Haskell is in</p> <ul> <li>WikiBooks, <em><a href="http://en.wikibooks.org/wiki/Haskell/Category_theory">Haskell/Category</a></em></li> </ul> <p>Further on the issue of the CS-style monads really being <a class="existingWikiWord" href="/nlab/show/strong+monads">strong monads</a>:</p> <ul> <li id="GLLN08"> <p><a class="existingWikiWord" href="/nlab/show/Jean+Goubault-Larrecq">Jean Goubault-Larrecq</a>, <a class="existingWikiWord" href="/nlab/show/Slawomir+Lasota">Slawomir Lasota</a>, <a class="existingWikiWord" href="/nlab/show/David+Nowak">David Nowak</a>, <em>Logical Relations for Monadic Types</em>, Mathematical Structures in Computer Science, <strong>18</strong> 6 (2008) 1169-1217 [<a href="https://arxiv.org/abs/cs/0511006">arXiv:cs/0511006</a>, <a href="https://doi.org/10.1017/S0960129508007172">doi:10.1017/S0960129508007172</a>]</p> </li> <li id="McDermottUustalu22"> <p><a class="existingWikiWord" href="/nlab/show/Dylan+McDermott">Dylan McDermott</a>, <a class="existingWikiWord" href="/nlab/show/Tarmo+Uustalu">Tarmo Uustalu</a>, <em>What Makes a Strong Monad?</em>, EPTCS <strong>360</strong> (2022) 113-133 [<a href="https://arxiv.org/abs/2207.00851">arXiv:2207.00851</a>, <a href="https://doi.org/10.4204/EPTCS.360.6">doi:10.4204/EPTCS.360.6</a>]</p> </li> </ul> <p>A comparison of monads with <a class="existingWikiWord" href="/nlab/show/applicative+functors">applicative functors</a> (also known as idioms) and with <a class="existingWikiWord" href="/nlab/show/arrows+%28in+computer+science%29">arrows (in computer science)</a> is in</p> <ul> <li>Exequiel Rivas, <em>Relating Idioms, Arrows and Monads from Monoidal Adjunctions</em>, (<a href="https://arxiv.org/abs/1807.04084">arXiv:1807.04084</a>)</li> </ul> <h3 id="in_quantum_computation">In quantum computation</h3> <p>Discussion of aspects of <a class="existingWikiWord" href="/nlab/show/quantum+computing">quantum computing</a> in terms of monads:</p> <ul> <li> <p>J. K. Vizzotto, <a class="existingWikiWord" href="/nlab/show/Thorsten+Altenkirch">Thorsten Altenkirch</a>, A. Sabry, <em>Structuring quantum effects: superoperators as arrows</em>, Mathematical Structures in Computer Science <strong>16</strong> 3 (2006) 453-468 [<a href="https://arxiv.org/abs/quant-ph/0501151">arXiv:quant-ph/0501151</a>, <a href="https://doi.org/10.1017/S0960129506005287">doi:10.1017/S0960129506005287</a>]</p> <blockquote> <p>(<a class="existingWikiWord" href="/nlab/show/superoperators">superoperators</a> as <a class="existingWikiWord" href="/nlab/show/arrows+in+computer+science">arrows in computer science</a>)</p> </blockquote> </li> </ul> <p>The <a class="existingWikiWord" href="/nlab/show/quantum+IO+monad">quantum IO monad</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Thorsten+Altenkirch">Thorsten Altenkirch</a>, <a class="existingWikiWord" href="/nlab/show/Alexander+Green">Alexander Green</a>, <em>The quantum IO monad</em>, Ch. 5 of: Simon Gay, Ian Mackie (eds.): <em>Semantic Techniques in Quantum Computation</em> (2010) 173-205 [<a href="http://www.cs.nott.ac.uk/~txa/publ/qio-chapter.pdf">pdf</a>, <a href="http://www.cs.nott.ac.uk/~txa/talks/qnet06.pdf">talk slides</a>, <a href="https://doi.org/10.1017/CBO9781139193313.006">doi:10.1017/CBO9781139193313.006</a>]</li> </ul> <p>Exposition:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Alexander+Green">Alexander Green</a>, <em>The Quantum IO Monad</em>, Nottingham (2007) [<a href="http://drinkupthyzider.co.uk/asg/pdfs/bctcs07.pdf">pdf</a>, <a class="existingWikiWord" href="/nlab/files/Green-QIOMonad.pdf" title="pdf">pdf</a> ]</li> </ul> <p>Implementation in <a class="existingWikiWord" href="/nlab/show/Haskell">Haskell</a>:</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Alexander+Green">Alexander Green</a>, <em><a href="https://hackage.haskell.org/package/QIO">hackage.haskell.org/package/QIO</a></em></li> </ul> <p>Much of the text and the diagrams in the entry above follow</p> <ul> <li><a class="existingWikiWord" href="/nlab/show/Hisham+Sati">Hisham Sati</a>, <a class="existingWikiWord" href="/nlab/show/Urs+Schreiber">Urs Schreiber</a>, <em><a class="existingWikiWord" href="/schreiber/show/The+Quantum+Monadology">The Quantum Monadology</a></em> [<a href="https://arxiv.org/abs/2310.15735">arXiv:2310.15735</a>]</li> </ul> </body></html> </div> <div class="revisedby"> <p> Last revised on December 27, 2024 at 21:34:58. See the <a href="/nlab/history/monad+%28in+computer+science%29" style="color: #005c19">history</a> of this page for a list of all contributions to it. </p> </div> <div class="navigation navfoot"> <a href="/nlab/edit/monad+%28in+computer+science%29" accesskey="E" class="navlink" id="edit" rel="nofollow">Edit</a><a href="https://nforum.ncatlab.org/discussion/15359/#Item_47">Discuss</a><span class="backintime"><a href="/nlab/revision/monad+%28in+computer+science%29/133" accesskey="B" class="navlinkbackintime" id="to_previous_revision" rel="nofollow">Previous revision</a></span><a href="/nlab/show/diff/monad+%28in+computer+science%29" accesskey="C" class="navlink" id="see_changes" rel="nofollow">Changes from previous revision</a><a href="/nlab/history/monad+%28in+computer+science%29" accesskey="S" class="navlink" id="history" rel="nofollow">History (133 revisions)</a> <a href="/nlab/show/monad+%28in+computer+science%29/cite" style="color: black">Cite</a> <a href="/nlab/print/monad+%28in+computer+science%29" accesskey="p" id="view_print" rel="nofollow">Print</a> <a href="/nlab/source/monad+%28in+computer+science%29" id="view_source" rel="nofollow">Source</a> </div> </div> <!-- Content --> </div> <!-- Container --> </body> </html>