6
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ Is it really that hard to believe that not every thing we can think of is an example of Curry-Howard correspondence? $\endgroup$ – Andrej Bauer Apr 10 at 11:54
  • 1
    $\begingroup$ 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. $\endgroup$ – Neel Krishnaswami Apr 10 at 13:55
  • 1
    $\begingroup$ A related Stack Overflow question I (somewhat clumsily) attempted to answer a while ago: Interesting operators in Haskell that obey modal axioms $\endgroup$ – duplode Apr 20 at 0:17
  • $\begingroup$ A lot more pointers are available in Modal Type Theory page on ncatlab. $\endgroup$ – Henry Story Apr 26 at 3:06
10
$\begingroup$

The two papers to look at it are Benton, Bierman and de Paiva's Computational Types from a Logical Perspective, 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, 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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Henry Story Apr 10 at 14:41
  • $\begingroup$ Categorical and Kripke Semantics for Constructive S4 Modal Logic, " 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. $\endgroup$ – Henry Story Apr 12 at 7:37
3
$\begingroup$

I'll add this in addition to Neel Krishnaswami's answer. The article he refers to A Judgemental Reconstruction of Modal Logic cites the article by Satoshi Kobayashi Monad As Modality which I had come across via Abramsky's article Game Semantics for Access Control. (That article then is built on in Game Semantics for Dependent Types 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.

$\endgroup$
  • 1
    $\begingroup$ 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, 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). $\endgroup$ – Neel Krishnaswami Apr 10 at 16:50
  • $\begingroup$ Ah yes. I had been wondering if Martin Abadi was aware of Kobayashi's paper in A Modal Deconstruction of Access Control Logics because he did not cite him. But he does site "Categorical and Kripke Semantics for Constructive S4 Modal Logic"! $\endgroup$ – Henry Story Apr 10 at 19:24
  • $\begingroup$ 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. $\endgroup$ – Henry Story Apr 10 at 19:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.