<p>I'll add this in addition to Neel Krishnaswami's answer. The article he refers to <a href="https://www.cs.cmu.edu/~fp/papers/mscs00.pdf" rel="noreferrer">A Judgemental Reconstruction of Modal Logic</a> cites the article by Satoshi Kobayashi <a href="https://www.sciencedirect.com/science/article/pii/S0304397596001697" rel="noreferrer">Monad As Modality</a> which I had come across via Abramsky's article <a href="https://www.sciencedirect.com/science/article/pii/S1571066109003107" rel="noreferrer">Game Semantics for Access Control</a>. (That article then is built on in <a href="https://link.springer.com/chapter/10.1007/978-3-662-47666-6_3" rel="noreferrer">Game Semantics for Dependent Types</a> to give a foundation for Homotopy Type Theory.)</p>

<p>I had not seen many citations of Kobayashi's work, which is why I asked the question here, because it seems really quite important. </p>

<p>Kobayashi argues that it is not because one can correctly analyse program logic with strong monads that this is the best way to do so. He finds that an extension of the concepts he calls L-Strong monads, that use a natural transformation with a built in co-monad gives the intuitive answer looked for. Given the right comonad <span class="math-container">$(L,\epsilon,\delta)$</span> the L-Strong monad comes with a natural transformation</p>

<p><span class="math-container">$t^L: LA \times MB \to M(LA \times B)$</span></p>

<p>giving rise to the following  modal logical rule:</p>

<p><span class="math-container">$\vdash ◻︎A \land \diamond B \supset \diamond(◻︎A \land B)$</span></p>

<p>Which is quite acceptable. It would give one for <span class="math-container">$A$</span>="2+2=4" and <span class="math-container">$B$</span>="S boards the plane" the reasoning from necessarily 2+2=4 and it is possible that S can board the plane one can conclude that it is possible that ( necessarily 2+2=4 and S boards the plane).</p>

<p>Kobayashi concludes his article with:</p>

<blockquote>
  <p>It is usually said that a constructive proof is a program. 
   However, exactly speaking, we should say that a constructive proof consists of a program and its correctness proof. 
   The correctness part is not necessary at runtime. 
   The realizability interpretation cuts off the correctness part (to some extent) and extracts the program part. 
   When we describe the specification of a program or prove a certain theorem in modal logic, we need the \nec-modality in general, because \nec\ is needed for correctness proofs. 
   However, the comonad types that model \nec-modality are not necessarily needed in the type system for the extracted programs, 
   because “the correctness part” is no longer needed.</p>
</blockquote>

CC BY-SA 4.0
2019-04-10T16:50:36.290Z
It's a bit unfortunate Kobayashi's paper is under-cited, but I think it's because most people end up citing Alechina, Mendler, de Paiva and Ritter's paper [*Categorical and Kripke Semantics for Constructive S4 Modal Logic*](https://www.cs.bham.ac.uk/~exr/papers/csl01.pdf), which uses Kobayashi's axiom as part of a sound and complete categorical axiomatization of CS4 (as well as duality results for Kripke and algebraic models on the model-theoretic side).
Neel Krishnaswami
CC BY-SA 4.0
2019-04-10T19:24:42.890Z
Ah yes. I had been wondering if Martin Abadi was aware of Kobayashi's paper in [A Modal Deconstruction of Access Control Logics](https://link.springer.com/chapter/10.1007/978-3-540-78499-9_16) because he did not cite him. But he does site "Categorical and Kripke Semantics for Constructive S4 Modal Logic"!
Henry Story
CC BY-SA 4.0
2019-04-10T19:29:47.810Z
I wonder if Kobayashi's article may be more helpful for Category Theoreticians or Computer Scientists, as they may not read that literature on modal logic. 

I came from to this from Scala programming, with a background in Modal Logic (David Lewis) and when I encountered Monads I really felt they had to be connected to the notion of contexts and tried to use them for access control. But when I expressed those thoughts I got weird looks. 
So I had to go off and learn category theory. The relation of necessity to comonads is I think really interesting, but it will take more time to digest.
Henry Story
CC BY-SA 4.0
2019-04-10T15:08:50.013Z
2019-04-10T15:08:50.013Z
Henry Story
<p>The two papers to look at it are Benton, Bierman and de Paiva's <a href="http://www.cs.bham.ac.uk/~vdp/publications/jfp.ps" rel="noreferrer"><em>Computational Types from a Logical Perspective</em></a>, which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's <a href="https://www.cs.cmu.edu/~fp/papers/mscs00.pdf" rel="noreferrer"><em>A Judgmental Reconstruction of Modal Logic</em></a>, which gives a constructive proof theory for S4 modal logic with box and diamond, and then translates Moggi's metalanguage into it.</p>

<p>Both papers note that the axioms of a strong monad were originally introduced by Curry in 1952, which was independently re-invented by Fairtlough and Mendler as <em>lax logic</em>. Giving the action on types and contexts below, we see:</p>

<p><span class="math-container">$$
\begin{array}{lcl}
( \to )^+ &amp; =&amp; ◻^+ \to ^+ \\
(◯)^+ &amp; = &amp; ◊◻^+ \\
^+ &amp; =&amp;  \;\;\mbox{for atomic}\;  \
\end{array}
$$</span></p>

<p>The translation of Davies and Pfenning is very similar to Gödel's embedding of intuitionistic logic into classical logic, and to Girard's embedding of intuitionistic logic into linear logic. </p>

CC BY-SA 4.0
2019-04-10T14:41:36.033Z
The interesting thing Mendlers' article on Lax Logic is that they state that the interpretation of ◯ modality a *local* modality.  

Interestingly In Mark Pfenning's Judngemental Reconstruction Article, they mention Kobayshi's "Monad as Modality" which I was going to use in an answer... Well perhaps I'll add it too, as then I can develop that part.
Henry Story
CC BY-SA 4.0
2019-04-12T07:37:51.053Z
[Categorical and Kripke Semantics for Constructive S4 Modal Logic](https://www.cs.bham.ac.uk/~exr/papers/csl01.pdf), " A Judgmental Reconstruction of Modal Logic" and Kobayashi's "Monad as Modality" agree I think that there are two logics that would fit the Monads in computer programming: Lax Logic and CS4. Kobayashi shows in Category Theoretic terms one gets the right results in Lax Logic, if one forgets about the correctness proof. Can one then choose which one to use when programming? Perhaps there is an interesting new question to ask on this topic.
Henry Story
CC BY-SA 4.0
2019-04-10T14:27:27.420Z
2019-04-10T14:27:27.420Z
Neel Krishnaswami
<p>According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad <span class="math-container">$(T, \eta, \mu)$</span> with T an functor and the two natural transformation 
<span class="math-container">$\eta: Id \to T$</span> and <span class="math-container">$\mu: T^2 \to T$</span> that arise out of an adjunction.  Monadic Equational Logic limits one to a single formula on each side of the turnstile such as <span class="math-container">$x_1 : \tau_1 \vdash_{pl} e: \tau_2$</span>. </p>

<p>In order to go beyond monadic equational logic to allow programs of the form 
<span class="math-container">$x_1: \tau_1, \dots, x_n:\tau_n \vdash e: \tau$</span> one needs an extra strength natural transformation </p>

<p><span class="math-container">$t_{A,B}: A \times TB \to T(A \times B)$</span></p>

<p>This allows one to take a context <span class="math-container">$\Gamma$</span> into account, represented by the <span class="math-container">$A$</span> in <span class="math-container">$t_{A,B}$</span> above.</p>

<p>This corresponds to the formula in modal logic</p>

<p><span class="math-container">$A \land \diamond B \supset \diamond(A \land B)$</span></p>

<p>which is logically quite weird as it would allow one to have propositions <span class="math-container">$A$</span>= "S can board the plane" and <span class="math-container">$B$</span>="S cannot board the plane" and reason "S can board the plane and it could have been the S cannot board the plane" to "it is possible that S can board the plane and that S cannot board the plane".</p>

<p>Moggi writes in his conclusion: </p>

<blockquote>
  <p>The semantics of computations corroborates the view that (constructive) proofs and programs are rather unrelated, although both of them can be understood in terms of functions. Indeed, monads (and comonads) used to model logical modalities, e.g. possibility and necessity in modal logic or why not and of course of linear logic, usually do not have a tensorial strength. In general, one should expect types suggested by logic to provide a more fine-grained type system without changing the nature of computations.</p>
</blockquote>

<p>Have I understood this correctly? Is the Curry-Howard isomorphism for monads illogical?</p>

CC BY-SA 4.0
2019-04-10T11:54:52.497Z
Is it really that hard to believe that not every thing we can think of is an example of Curry-Howard correspondence?
Andrej Bauer
CC BY-SA 4.0
2019-04-10T13:55:48.883Z
If it's not an instance of the CH correspondence, there is work to be done to **make** it into an instance. The effort will probably teach new things both about logic, and about computation.
Neel Krishnaswami
CC BY-SA 4.0
2019-04-20T00:17:47.123Z
A related Stack Overflow question I (somewhat clumsily) attempted to answer a while ago: [*Interesting operators in Haskell that obey modal axioms*](https://stackoverflow.com/q/49262771/2751851)
duplode
CC BY-SA 4.0
2019-04-26T03:06:51.870Z
A lot more pointers are available in [Modal Type Theory](https://ncatlab.org/nlab/show/modal+type+theory) page on ncatlab.
Henry Story
<lo.logic><functional-programming><ct.category-theory><monad><comonad>
What logic correponds via Curry-Howard to a Monad?
Henry Story
# What logic correponds via Curry-Howard to a Monad?

(Asked by: username_0 on 2019-04-10)

According to Moggi's 1991 paper "Notions of computation and monads" one can represent monadic equational logic with the well known monad $(T, \eta, \mu)$ with T an functor and the two natural transformation
$\eta: Id \to T$ and $\mu: T^2 \to T$ that arise out of an adjunction. Monadic Equational Logic limits one to a single formula on each side of the turnstile such as $x\_1 : \tau\_1 \vdash\_{pl} e: \tau\_2$.

In order to go beyond monadic equational logic to allow programs of the form
$x\_1: \tau\_1, \dots, x\_n:\tau\_n \vdash e: \tau$ one needs an extra strength natural transformation

$t\_{A,B}: A \times TB \to T(A \times B)$

This allows one to take a context $\Gamma$ into account, represented by the $A$ in $t\_{A,B}$ above.

This corresponds to the formula in modal logic

$A \land \diamond B \supset \diamond(A \land B)$

which is logically quite weird as it would allow one to have propositions $A$= "S can board the plane" and $B$="S cannot board the plane" and reason "S can board the plane and it could have been the S cannot board the plane" to "it is possible that S can board the plane and that S cannot board the plane".

Moggi writes in his conclusion:

> The semantics of computations corroborates the view that (constructive) proofs and programs are rather unrelated, although both of them can be understood in terms of functions. Indeed, monads (and comonads) used to model logical modalities, e.g. possibility and necessity in modal logic or why not and of course of linear logic, usually do not have a tensorial strength. In general, one should expect types suggested by logic to provide a more fine-grained type system without changing the nature of computations.

Have I understood this correctly? Is the Curry-Howard isomorphism for monads illogical?

**Tags:** lo.logic, functional-programming, ct.category-theory, monad, comonad
> **Comments:**
> **username_1**: Is it really that hard to believe that not every thing we can think of is an example of Curry-Howard correspondence?  
> **username_2**: If it's not an instance of the CH correspondence, there is work to be done to **make** it into an instance. The effort will probably teach new things both about logic, and about computation.  
> **username_3**: A related Stack Overflow question I (somewhat clumsily) attempted to answer a while ago: [*Interesting operators in Haskell that obey modal axioms*](https://stackoverflow.com/q/49262771/2751851)  
> **username_0**: A lot more pointers are available in [Modal Type Theory](https://ncatlab.org/nlab/show/modal+type+theory) page on ncatlab.  

---

## 2 answers

### Answer by username_2 on 2019-04-10. Score: 15 | Accepted answer

The two papers to look at it are Benton, Bierman and de Paiva's [*Computational Types from a Logical Perspective*](http://www.cs.bham.ac.uk/~vdp/publications/jfp.ps), which directly gives a proof theory for Moggi's computational lambda-calculus; and Rowan Davies and Frank Pfenning's [*A Judgmental Reconstruction of Modal Logic*](https://www.cs.cmu.edu/~fp/papers/mscs00.pdf), which gives a constructive proof theory for S4 modal logic with box and diamond, and then translates Moggi's metalanguage into it.

Both papers note that the axioms of a strong monad were originally introduced by Curry in 1952, which was independently re-invented by Fairtlough and Mendler as *lax logic*. Giving the action on types and contexts below, we see:

$$
\begin{array}{lcl}
( \to )^+ & =& ◻^+ \to ^+ \\
(◯)^+ & = & ◊◻^+ \\
^+ & =& \;\;\mbox{for atomic}\; \
\end{array}
$$

The translation of Davies and Pfenning is very similar to Gödel's embedding of intuitionistic logic into classical logic, and to Girard's embedding of intuitionistic logic into linear logic.

> **Comments:**
> **username_0**: The interesting thing Mendlers' article on Lax Logic is that they state that the interpretation of ◯ modality a *local* modality.    Interestingly In Mark Pfenning's Judngemental Reconstruction Article, they mention Kobayshi's "Monad as Modality" which I was going to use in an answer... Well perhaps I'll add it too, as then I can develop that part.  
> **username_0**: [Categorical and Kripke Semantics for Constructive S4 Modal Logic](https://www.cs.bham.ac.uk/~exr/papers/csl01.pdf), " A Judgmental Reconstruction of Modal Logic" and Kobayashi's "Monad as Modality" agree I think that there are two logics that would fit the Monads in computer programming: Lax Logic and CS4. Kobayashi shows in Category Theoretic terms one gets the right results in Lax Logic, if one forgets about the correctness proof. Can one then choose which one to use when programming? Perhaps there is an interesting new question to ask on this topic.  

---

### Answer by username_0 on 2019-04-10. Score: 5

I'll add this in addition to Neel Krishnaswami's answer. The article he refers to [A Judgemental Reconstruction of Modal Logic](https://www.cs.cmu.edu/~fp/papers/mscs00.pdf) cites the article by Satoshi Kobayashi [Monad As Modality](https://www.sciencedirect.com/science/article/pii/S0304397596001697) which I had come across via Abramsky's article [Game Semantics for Access Control](https://www.sciencedirect.com/science/article/pii/S1571066109003107). (That article then is built on in [Game Semantics for Dependent Types](https://link.springer.com/chapter/10.1007/978-3-662-47666-6_3) to give a foundation for Homotopy Type Theory.)

I had not seen many citations of Kobayashi's work, which is why I asked the question here, because it seems really quite important.

Kobayashi argues that it is not because one can correctly analyse program logic with strong monads that this is the best way to do so. He finds that an extension of the concepts he calls L-Strong monads, that use a natural transformation with a built in co-monad gives the intuitive answer looked for. Given the right comonad $(L,\epsilon,\delta)$ the L-Strong monad comes with a natural transformation

$t^L: LA \times MB \to M(LA \times B)$

giving rise to the following modal logical rule:

$\vdash ◻︎A \land \diamond B \supset \diamond(◻︎A \land B)$

Which is quite acceptable. It would give one for $A$="2+2=4" and $B$="S boards the plane" the reasoning from necessarily 2+2=4 and it is possible that S can board the plane one can conclude that it is possible that ( necessarily 2+2=4 and S boards the plane).

Kobayashi concludes his article with:

> It is usually said that a constructive proof is a program.
> However, exactly speaking, we should say that a constructive proof consists of a program and its correctness proof.
> The correctness part is not necessary at runtime.
> The realizability interpretation cuts off the correctness part (to some extent) and extracts the program part.
> When we describe the specification of a program or prove a certain theorem in modal logic, we need the \nec-modality in general, because \nec\ is needed for correctness proofs.
> However, the comonad types that model \nec-modality are not necessarily needed in the type system for the extracted programs,
> because “the correctness part” is no longer needed.

> **Comments:**
> **username_2**: It's a bit unfortunate Kobayashi's paper is under-cited, but I think it's because most people end up citing Alechina, Mendler, de Paiva and Ritter's paper [*Categorical and Kripke Semantics for Constructive S4 Modal Logic*](https://www.cs.bham.ac.uk/~exr/papers/csl01.pdf), which uses Kobayashi's axiom as part of a sound and complete categorical axiomatization of CS4 (as well as duality results for Kripke and algebraic models on the model-theoretic side).  
> **username_0**: Ah yes. I had been wondering if Martin Abadi was aware of Kobayashi's paper in [A Modal Deconstruction of Access Control Logics](https://link.springer.com/chapter/10.1007/978-3-540-78499-9_16) because he did not cite him. But he does site "Categorical and Kripke Semantics for Constructive S4 Modal Logic"!  
> **username_0**: I wonder if Kobayashi's article may be more helpful for Category Theoreticians or Computer Scientists, as they may not read that literature on modal logic.   I came from to this from Scala programming, with a background in Modal Logic (David Lewis) and when I encountered Monads I really felt they had to be connected to the notion of contexts and tried to use them for access control. But when I expressed those thoughts I got weird looks.  So I had to go off and learn category theory. The relation of necessity to comonads is I think really interesting, but it will take more time to digest.  

---

