Monad as Modality

Satoshi KOBAYASHI^{∗}

Abstract

In 1989, E. Moggi proposed a general categorical framework for program semantics based on the notion of (strong) monads. Since his construction was not in harmony with categorical semantics of modal logics, he thought that Curry-Howard correspondence does not hold between constructive proofs in modal logics and programs. However, contrary to his thought, we can generalize his semantics and make it compatible with modal logic semantics. Moreover, we show that Curry-Howard correspondence actually holds. Using this result, we can extract monad-based imperative functional programs from constructive proofs in modal logics.

1 Introduction

In 1989, E. Moggi proposed a categorical framework for program semantics based on the notion of strong monads. His framework is so general that it can treat various kinds of computation such as non-terminating evaluation, nondeterministic computation, side-effects, exceptions, continuation passing, I/O, etc. Today, based on this work, monad-based imperative functional programs are actively studied by many researchers.

It is known that monads can be used to interpret logical modalities such as possibility in modal logic or ‘why not’ of linear logic. Comonads, the dual of monads, are used to model necessity or ‘of course’ modality. However, strong monads are not suitable for modeling modalities. The reason is that if we interpret modalities in strong monad, some very unnatural formulas such as A ∧ ◇B → ◇(A ∧ B) are validated. In this sense, strong monads are too strong. However, simple monads are too weak to be used as a basis of program semantics. So Moggi thought that programs and constructive proofs are rather unrelated. If this thought was true, formal program derivation techniques based on proofs-as-programs principle (so called Curry-Howard principle) would not be generalized to derive monad-based imperative programs.

∗Department of Applied Mathematics and Informatics, Ryukoku University, Seta, Ohtsu, 520-21, Japan. phone: 775-43-7528 (office), -7523 (department secretary), fax: 775-43-7524, e-mail: satoshi@rins.ryukoku.ac.jp

However, fortunately, that thought has turned out to be false. In this manuscript, we introduce the notion of L-strong monad which is a generalization of strong monad. Using this notion, we can generalize Moggi’s framework and make it suitable as a semantical foundation for both programs and (some kind of) modal logics. Moreover, we show that modal logic proofs are actually considered as programs. As an application of this result, we can extract imperative functional programs from proofs in constructive modal logics.

In section 2, we give a brief review of Moggi’s semantics. In section 3, we introduce the notion of L-strong monad and generalize Moggi’s semantics preserving soundness and completeness. In section 4, a constructive version of S4 modal logic called CS4 is introduced. We show that L-strong monad gives a complete semantics of this logic. In section 5, we define a realizability interpretation of CS4 and prove its soundness. Using this result, we show that proofs in CS4 can be considered as programs.

2 Moggi’s Semantics

The central idea of Moggi’s program semantics is that we distinguish the object A of values of type A from the object MA of computations of type A, where A and B are semantical domains corresponding to A and B respectively. An “impure” function f from A to B is modeled by a morphism [[f]] from A to MB. Intuitively, an element α of MA is a computation which may produce a value in A as the resulting value. α itself is not a value in A. α and its resulting value are not identified. As examples in the category of sets, partiality is modeled by taking MA = A_{⊥}, nondeterminism is modeled by taking MA = P(A) (the power set of A), etc. For details and further examples, see [5]. We call M a notion of computation.

An important discovery of Moggi is that for many interesting cases, M and associated operations form a strong monad structure. Moggi found a general framework of program semantics based on the notion of strong monad.

In this manuscript, we assume the reader is familiar to elementary category theory and monads and comonads. However, knowledge on strong monad is not assumed. In the following, we write f^{∗} and g^{∧} to mean Kleisli lifting of f and co-Kleisli lifting of g respectively. f;^{L} g means composition in co-Kleisli category.

Definition 2.1 Let C be a cartesian category and M be an endofunctor on it. A tensorial strength for M is a natural transformation t : –×M(–) → M(–×–) satisfying the following conditions:

t_{1,A}; M(r_{A}) = r_{MA}, t_{A×B,C}; M(α_{A,B,C}) = α_{A,B,MC}; (id_{A} × t_{B,C}); t_{A,B×C},

where r and α are natural isomorphisms

r_{A} : 1 × A → A, α_{A,B,C} : (A × B) × C → A × (B × C).

Actually tensorial strength can be defined in more general setting. However, the above definition suffices for our purpose.

Definition 2.2 A strong monad over a cartesian category C is a quadruple (M, η, μ, t) satisfying the following conditions:

1. (M, η, μ) is a monad over C,

2. t is a tensorial strength for M,

3. the following two equations hold:

(id_{A} × η_{B}); t_{A,B} = η_{A×B}, (id_{A} × μ_{B}); t_{A,B} = t_{A,MB}; M(t_{A,B}); μ_{A×B}.

Example: Here we present only one example which will be important later. A side effect monad is a strong monad over the category of sets defined as follows: let S be the set of states, then define

M(–) = P(S × (– × S))
(s, (a′, s′)) ∈ η_{A}(a) ⟺ a′ = a ∧ s′ = s
(s, (a′′, s′′)) ∈ μ_{A}(a) ⟺ ∃a′.∃s′.(s, (a′, s′)) ∈ a ∧ (s′, (a′′, s′′)) ∈ a′,
(s, (a′, s′)) ∈ t_{A,B}(a, b) ⟺ ∃b′.((s, (b′, s′)) ∈ b ∧ a′ = (a, b′)),

where P is the covariant power set functor. Intuitive meaning of (s, (a′, s′)) ∈ a is that evaluation of a, started at state s, may terminate at state s′ and return the resulting value a′.

2.1 Computational Metalanguage

In [5], Moggi proposed a formal language called Computational Metalanguage. The approach taken in [5] is as follows: first he establishes a clear categorical semantics of this metalanguage, and then describe the semantics of other languages in terms of metalanguage. Types: Assume the set of basic types is given. Then the types of the language are defined by the following rules: (1) each basic type is a type, (2) 1 is a type,

(3) if τ_{1} and τ_{2} are types, then τ_{1} × τ_{2} is a type, (4) if τ is a type, then Mτ is a type. Terms: Suppose the set of function constants are given and each function constant has its arity of the form τ_{1} → τ_{2}, where τ_{1} and τ_{2} are types. Then, terms are defined by the following rules.

{⊢ τ_{i} type (1 ≤ i ≤ n) \atop x_{i} : τ_{1}, …, x_{n} : τ_{n} ⊢ x_{i} : τ_{i}}  Γ ⊢ ∗ : 1

\begin{matrix}Γ ⊢ e_{1} : τ_{1} & Γ ⊢ e_{2} : τ_{2} \\ Γ ⊢ ⟨e_{1}, e_{2}⟩ : τ_{1} × τ_{2} \end{matrix}  {Γ ⊢ e : τ_{1} × τ_{2} \atop Γ ⊢ π_{i}(e) : τ_{i}}

{Γ ⊢ e_{1} : τ_{1} \atop Γ ⊢ f(e_{1}) : τ_{2}} (f is a constant of arity τ_{1} → τ_{2})  {Γ ⊢ e : τ \atop Γ ⊢ [e] : Mτ}
Γ ⊢ e_{1} : Mτ_{1} Γ, x : τ_{1} ⊢ e_{2} : Mτ_{2}
Γ ⊢ (let x_{1} ⇐ e_{1} in e_{2}) : Mτ_{2}

Intuitively, [a] : MA is a : A viewed as a computation, and execution of (letx_{1} ⇐ e_{1} ine_{2}) is done as follows: first execute e_{1} and bind x_{1} to the resulting value v_{1}, then execute e_{2} in the new environment and get the resulting value v_{2}, finally return v_{2} as the resulting value of the whole execution.

2.2 Semantics

Types: Suppose a strong monad (M, η, μ, t) over a cartesian category C is given. For each basic type τ, define [[τ]] as an arbitrary object in C. For the other types, [[–]] is defined by the following inductive definition:

[[Mτ]] = M[[τ]], [[1]] = 1, [[τ_{1} × τ_{2}]] = [[τ_{1}]] × [[τ_{2}]].

For a context Γ = x_{1} : τ_{1}, …, x_{n} : τ_{n}, we define [[Γ]] = [[τ_{1}]] × ⋯ × [[τ_{n}]]. Terms: For a term e for which Γ ⊢ e : τ is derivable, its interpretation [[Γ ⊢ e : τ]] is defined as a morphism from [[Γ]] to [[τ]].

First, we interpret function symbol f of arity τ_{1} → τ_{2} by an arbitrary morphism [[f]] from [[τ_{1}]] to [[τ_{2}]]. Then [[Γ ⊢ e : τ]] is defined by induction on the derivation of Γ ⊢ e : τ.

Variables, ∗, pairing, projections and function call f(e) are interpreted as usual. [[Γ ⊢ [e] : Mτ]] is defined as [[Γ ⊢ e : τ]]; η_{[[τ]]}. Interpretation of let expressions is the keypoint of Moggi’s semantics. Suppose

[[Γ ⊢ e_{1} : Mτ_{1}]] = g_{1} : [[Γ]] → M[[τ_{1}]],
[[Γ, x_{1} : τ_{1} ⊢ e_{2} : Mτ_{2}]] = g_{2} : [[Γ]] × [[τ_{1}]] → M[[τ_{2}]].

At the first sight, definition

[[Γ ⊢ (let x_{1} ⇐ e_{1} in e_{2}) : Mτ_{2}]] = ⟨id_{[[Γ]]}, g_{1}⟩; g_{2}^{∗} : [[Γ]] → M[[τ_{2}]],

seems to work. However, since the codomain of ⟨id_{[[Γ]]}, g_{1}⟩ is [[Γ]] × M[[τ_{1}]] and the domain of g_{2}^{∗} is M([[Γ]] × [[τ_{1}]]), we can not compose ⟨id_{[[Γ]]}, g_{1}⟩ and g_{2}^{∗}. So here we need tensorial strength. Since t_{[[Γ]],[[τ_{1}]]} is a morphism from [[Γ]] × M[[τ_{1}]] to M([[Γ]] × [[τ_{1}]]), we can compose ⟨id_{[[Γ]]}, g_{1}⟩ and t_{[[Γ]],[[τ_{1}]]}; g_{2}^{∗}. So we define

[[Γ ⊢ (let x_{1} ⇐ e_{1} in e_{2}) : Mτ_{2}]] = ⟨id_{[[Γ]]}, g_{1}⟩; t_{[[Γ]],[[τ_{1}]]}; g_{2}^{∗} : [[Γ]] → M[[τ_{2}]].

This semantics is summarized in Table 1 in Appendix.

2.3 Formal System for Equality Judgment

Moggi[5] proposed a formal system for judging equality of terms. It has judgments of the form Γ ⊢ e_{1} =_{τ} e_{2}. Inference rules of this system is summarized in Table 2 in Appendix. The interpretation of judgments is as follows: Γ ⊢ e_{1} =_{τ} e_{2} is true if and only if [[Γ ⊢ e_{1} : τ]] = [[Γ ⊢ e_{2} : τ]] holds.

Theorem 2.3 (Moggi) This formal system is sound and complete with respect to the semantics given in the above.

3 Generalized Semantics

In this section we generalize Moggi’s semantics based on the notion of L-strong monad.

Definition 3.1 A cartesian comonad over a cartesian category C is a comonad which preserves the cartesian structure of C. In detail, it is a comonad equipped with an isomorphism m_{1} : 1 → L1 and a natural isomorphism m : L(–)×L(–) → L(– × –) satisfying m_{A,B}^{−1} = ⟨L(π_{A}^{A,B}), L(π_{B}^{A,B})⟩ : L(A × B) → LA × LB.

An important fact is that the co-Kleisli category C^{L} induced by a cartesian comonad is cartesian. Its cartesian structure is given as follows: product A ×^{L}

B = A × B, pairing ⟨f, g⟩^{L} = ⟨f, g⟩, projection πi^{L} = ε_{A_{1}×A_{2}}; π_{i} : L(A_{1} × A_{2}) →

A_{i}, terminal object 1^{L} = 1, terminal morphism !A^{L} =!_{LA} : LA → 1.

Definition 3.2 Let (L, ε, δ, m, m_{1}) be a cartesian comonad over C and M be an endofunctor on C. Consider two functors H, K : C^{L} × C → C defined by the following:

H(A, B) = LA × MB, K(A, B) = M(LA × B) for objects A, B,
H(f, g) = f^{∧} × Mg,  K(f, g) = M(f^{∧} × g)  for morphisms f, g.

An L-tensorial strength (L-strength for short) for M is, by definition, a natural transformation t^{L} from H to K satisfying the following conditions:

\begin{matrix}t_{1,A}^{L}; M(rA^{L}) = rMA^{L}, \\ t_{A×B,C}^{L}; M(α_{A,B,C}^{L}) = α_{A,B,MC}^{L}; (id_{LA} × t_{B,C}^{L}); t_{A,LB×C}^{L}, \end{matrix}

where r^{L} and α^{L} are natural isomorphisms

\begin{matrix}rA^{L} = π_{A}^{L1,A} : L1 × A → A, \\ α_{A,B,C}^{L} = (m_{A,B}^{−1} × id_{C}); α_{LA,LB,LC} : L(A × B) × C → LA × (LB × C). \end{matrix}

Definition 3.3 An L-strong monad over a cartesian category C is a triple (M, L, t^{L}) satisfying the following conditions:

1. L = (L, ε, δ, m, m_{1}) is a cartesian comonad over C,

2. M = (M, η, μ) is a monad over C,

3. t^{L} is a L-tensorial strength for M,

4. the following two equations hold:

(id_{LA} × η_{B}); t_{A,B}^{L} = η_{LA×B}
(id_{LA} × μ_{B}); t_{A,B}^{L} = t_{A,MB}^{L}; M(t_{A,B}^{L}); μ_{LA×B} □

Note that strong monad is a special case of L-strong monad of which comonad structure is trivial.

3.1 L-strong Monad Semantics

Now, let us define a new semantics. Types: Our interpretation of types is the same as Moggi’s except that [[Mτ]] is defined as ML[[τ]]. Terms: We define [[Γ ⊢ e : τ]] as a morphism from L[[Γ]] to [[τ]]. That is, it is defined as a morphism from [[Γ]] to [[τ]] in the co-Kleisli category C^{L}. Our interpretation is defined so that it coincides with Moggi’s one when the comonad structure is trivial.

Function symbol f of arity τ_{1} → τ_{2} is arbitrarily interpreted by a morphism [[f]] : L[[τ_{1}]] → [[τ_{2}]].

Interpretation of variables, ∗, pairing, projections and function call f(e) is easy (see Table 3), since C^{L} is cartesian. [[Γ ⊢ [e] : Mτ]] is defined as [[Γ ⊢ e : τ]];^{L} η_{L[[τ]]}. Let expressions are interpreted as follows: suppose

[[Γ ⊢ e_{1} : Mτ_{1}]] = g_{1} : L[[Γ]] → ML[[τ_{1}]],
[[Γ, x_{1} : τ_{1} ⊢ e_{2} : Mτ_{2}]] = g_{2} : L([[Γ]] × [[τ_{1}]]) → ML[[τ_{2}]],

then we define

[[Γ ⊢ (let x_{1} ⇐ e_{1} in e_{2}) : Mτ_{2}]] = ⟨id_{L[[Γ]]}, g_{1}⟩; t_{[[Γ]],L[[τ_{1}]]}^{L}; (m_{[[Γ]],[[τ_{1}]]}; g_{2})^{∗}
: L[[Γ]] → ML[[τ_{2}]].

Note that L-tensorial strength is used here in place of tensorial strength. Equality Judgment: We define that Γ ⊢ e_{1} =_{τ} e_{2} is true if and only if [[Γ ⊢ e_{1} : τ]] = [[Γ ⊢ e_{2} : τ]] holds.

Theorem 3.4 The formal system given in Table 2 in Appendix is sound and complete for the above interpretation.

Proof. Soundness is proved by tedious diagram chasing. Completeness is trivial, since our semantics contains Moggi’s one as a special case.

4 Constructive Modal Logic

In this section, we consider a constructive propositional modal logic called CS4, which corresponds to the notion of L-strong monad. Language, Axioms and Rules: CS4 has ∧, ∨, → as propositional connectives, ⊥ as a propositional constant, and □, ◇ as modal operators. Its axioms and rules are as follows:

1. it has all axioms and rules of intuitionistic propositional logic.

2. it has the necessitation rule for □, i.e., if A is a theorem, then □A is also a theorem.

3. it has the following seven axioms on modality:

□-K: □(A → B) → (□A → □B)  ◇-K: □(A → B) → (◇A → ◇B)
□-T: □A → A  ◇-T: A → ◇A
□-4: □A → □^{2}A  ◇-4: ◇^{2}A → ◇A
◇⊥-E: ◇⊥ → A.

To simplify the arguments, we shall consider the □◇∧→-fragment of CS4 in this manuscript. So the axiom ◇⊥-E is not considered. The full set version of CS4 will be treated in the full paper.

4.1 Categorical Semantics

Let us give a categorical semantics of CS4 based on L-strong monad. Suppose that a L-strong monad (M, L, t^{L}) over a cartesian closed category C is given. Cartesian closed-ness is needed for interpreting implication.

First, each propositional variable P is interpreted by an arbitrary object [[P]] in C. Then [[–]] is extended to all propositions as follows:

\begin{matrix}[[A ∧ B]] = & [[A]] × [[B]], & [[A → B]] = & [[B]]^{[[A]]}, \\ [[□A]] = & L[[A]], & [[◇A]] = & M[[A]]. \end{matrix}

For Γ = A_{1}, …, A_{n}, define [[Γ]] = [[A_{1}]] × ⋯ × [[A_{n}]]. If n = 0, [[Γ]] = 1. This interpretation is sound and complete in the following sense:

Theorem 4.1 (1) If Γ ⊢ A in CS4, there exists a morphism from [[Γ]] to [[A]].

(2) If Γ ⊬ A in CS4, there exists a model in which no morphisms are from [[Γ]] to [[A]].

5 Curry-Howard Principle

In this section, we show how proofs in CS4 are considered as programs. We define a realizability interpretation of CS4 and prove that we can extract a program from a proof using realizability. The target programming language is Moggi’s computational metalanguage. In order to interpret implicational formulas, we extend the language by adding function type A → B, λ-abstraction λx : A.e and function application e_{1}e_{2}. For the details of this extension, see [5].

First we provide some notations. Suppose a strong monad over a cartesian closed category is given. We define

\overline{A} = \{ e | e : 1 → A \}, Cmd = ⋃\{ \overline{MA} | A is an object \}.

We call an element of Cmd a command, since a term of type MA is considered as a computation. Suppose that S is the set of global states. We assume that for each e in \overline{MA}, a binary relation R_{e}⊆ S × (\overline{A} × S) is given and the following three conditions hold:

(i) R_{a;η_{A}}= { (s, (a, s)) | s ∈ S }, (ii) R_{a;f^{∗}}= { (s, (b, s′′)) | ∃a′.∃s′.(s, (a′, s′)) ∈R_{a} ∧(s′, (b, s′′)) ∈R_{a′;f} } (iii) R_{⟨a,b⟩;t_{A,B}}= { (s, (c, s′)) | ∃b′.(s, (b′, s′)) ∈R_{b} ∧c = ⟨a, b′⟩ } For example, in side effect monad, each global element of MA is naturally identified with such a binary relation as above. We adopt the following abbreviations:

s ≻^{e} s′ ⟺ ∃e′.(s R_{e} (e′, s′)), s ≻ s′ ⟺ ∃e.(s ≻^{e} s′).

Informally speaking, the ideas behind our realizability interpretation is as follows. We consider that ◇A means that there exists a command e such that the execution of e terminates, and whenever it terminates, A becomes true.^{1} Then the realizer of ◇A must give a command e and a realizer a which realizes A after the termination of e. Since the truth of A depends on the states and e may be non-deterministic, realizer a must be chosen depending on how e has been executed. So it is natural to think that a is returned by e as the resulting value. That is, we consider that a realizer of ◇A is a command e ∈ \overline{MA} which terminates and returns a realizer of A. Next, we consider that □A means that for all command e, whenever e terminates, A becomes true. Then it is natural to consider that a realizer of □A is such a that for all command e, a realizes A after the termination of e. So the type of realizers of □A will be the same as that of A. We need no comonad types to define the realizability of □A. Along these lines, we give the formal definition of realizability. Type of Realizers: First, we arbitrarily choose two functions ρ and r so that ρ(P) be an object of the given category and r(s, P) be a subset of \overline{ρ(P)} for each propositional variable P and state s. Next we extend ρ to all propositions as follows:

\begin{matrix}ρ(A ∧ B) = & ρ(A) × ρ(B), & ρ(A → B) = & ρ(B)^{ρ(A)}, \\ ρ(□A) = & ρ(A), & ρ(◇A) = & Mρ(A). \end{matrix}

Set of Realizers: We extend r as follows:

r(s, A ∧ B) = { ⟨a, b⟩ | a ∈ r(s, A) ∧ b ∈ r(s, B) },
r(s, A → B) = \{ e ∈ \overline{ρ(A → B)} | ∀a ∈ r(s, A).(e`a ∈ r(s, B)) \},
r(s, □A) = \{ e ∈ \overline{ρ(□A)} | ∀s′ ∈ S.(s ≻ s′ → e ∈ r(s′, A)) \},

1This explanation is not very accurate. To be more accurate, we must give a Kripke style semantics of CS4. It will be given in the full paper.

r(s, ◇A) = \{ e ∈ \overline{ρ(◇A)} | (∃s′.s ≻^{e} s′) ∧

∀e′.∀s′.(s ≻^{e} (e′, s′) → e′ ∈ r(s′, A)) },

where e`a is an abbreviation of ⟨e, a⟩; eval. Note that r(s, A) is defined as a subset of \overline{ρ(A)}. r(s, A) is the set of realizers of A at s. We write e r_{s} A for e ∈ r(s, A) and read it as “e realizes A at state s”. We assume that each term f of computational metalanguage is interpreted by a morphism [[f]] in the given strong monad according to Moggi’s semantics. For a term with ⊢ f : 1 → ρ(A), we define f r_{s} A ⟺ [[f]] r_{s} A. f r A means, by definition, f r_{s} A holds for any s ∈ S. A formula A is called realizable if f r A holds for some term f.

Let T be a theory given by adding some realizable formulas to CS4 as axioms. Then the following theorem holds.

Theorem 5.1 If ⊢ A in T, we have f r A for some term f.

Application: Let T be a theory such as above. Then if ◇A is proved in T, we can find a program e written in computational metalanguage such that when e is executed, it necessarily terminates and A becomes realizable after the termination of e.

6 Conclusion

There are two kinds of type systems in the world: one can be viewed as natural logics, and the other can not be. Moggi’s type system is of the latter type. It can not be a natural modal logic. If we want to make it natural, we must make some modifications and add comonad type LA to it. Then we will have a type system corresponding to constructive S4 modal logic.

It is often said that constructive proofs are programs. However, exactly speaking, we should say that a constructive proof consists of a program and its correctness proof. Correctness part is not necessary in runtime. Realizability interpretation cuts off the correctness part (to some extent) and extract a program part. When we describe the specification of a program or prove a certain theorem in modal logic, we need □-modality in general, because □ is needed for correctness proof. However, comonad types which models □-modality is not necessarily needed in type systems for extracted programs, since “correctness part” is no longer needed.

We meet a similar situation when considering dependent types. Constructive type systems designed for proof development usually have dependent product Πx.A(x) and dependent sum Σx.A(x) for encoding quantification. However, we can “collapse” these types to simple function space and simple binary products, when extracting programs from proofs. Dependent types are not necessarily needed in type systems for programs. They are needed for doing logic. We think that comonad type LA is collapsed to A for the same reason.

Since the truth of a proposition in modal logic may depend on states, type system for modal logic should have state-dependent types. However, type systems for programming languages usually have no such types. This explains why Γ ⊢ e : Mτ is interpreted as a morphism f from L[[Γ]] to ML[[τ]] in our semantics. An object of the form LA is considered to be a state-independent type. f takes its argument from state-independent type L[[Γ]] and gives a computation in ML[[τ]]. This computation returns, when evaluated, a resulting value in state-independent type L[[τ]].

7 Related Works

Bierman et al.[1] study constructive S4 logic without ◇ modality. They propose a sequent calculus formulation and a natural deduction formulation of this logic and give term-assignment systems for them. They also give a categorical semantics of this logic using cartesian comonads.

Wijesekera[6] studies a constructive version of K modal logic, which is a subsystem of CS4. Kripke semantics is given for this logic and completeness theorem is proved.

In our semantics, comonads have logical meaning only and have no computational meaning. Brookes and Geva[2] introduced the notion of computational comonad and used it to model intensional aspects of computation. However, computational comonads can not model □-modality. Because every computational comonad must have a natural transformation γ : Id_{C} → L and hence validates □A ↔ A.

References

[1] Bierman, G. et al: Intuitionistic Necessity Revisited (Extended Abstract), distributed via anonymous ftp.

[2] Brookes, S. and Geva, S.: Computational Comonads and Intensional Semantics, In Applications of Categories in Computer Science, London Mathematical Society Lecture Notes Series, Vol. 177.

[3] Kock, A.: Strong Functors and Monoidal Monads, Arch. Math. 23, 1972.

[4] Moggi, E.: Computational lambda-calculus and monads, In IEEE Symposium on Logic in Computer Science, 1989.

[5] Moggi, E.: Notions of Computation and Monads, Information and Computation, Vol. 93, (1991), pp. 55–92.

[6] Wijesekera, D.: Constructive Modal Logics I, Annals of Pure and Applied Logic 50 (1990), pp.271–301.

Appendix

Syntax  Semantics

⊢ τ_{i} type (1 ≤ i ≤ n)

x_{i} : τ_{1}, …, x_{n} : τ_{n} ⊢ x_{i} : τ_{i}  ⇔ π_{i}
Γ ⊢ ∗ : 1  ⇔ !_{[[Γ]]}
Γ ⊢ e_{1} : τ_{1}  ⇔ g_{1}
Γ ⊢ e_{2} : τ_{2}  ⇔ g_{2}
Γ ⊢ ⟨e_{1}, e_{2}⟩ : τ_{1} × τ_{2}  ⇔ ⟨g_{1}, g_{2}⟩
Γ ⊢ e : τ_{1} × τ_{2}  ⇔ g
Γ ⊢ π_{i}(e) : τ_{i}  ⇔ g; π_{i}

f : τ_{1} → τ_{2} (constant)

Γ ⊢ e_{1} : τ_{1}  ⇔ g
Γ ⊢ f(e_{1}) : τ_{2}  ⇔ g; [[f]]
Γ ⊢ e : τ  ⇔ g
Γ ⊢ [e] : Mτ  ⇔ g; η_{[[τ]]}
Γ ⊢ e_{1} : Mτ_{1}  ⇔ g_{1}
Γ, x : τ_{1} ⊢ e_{2} : Mτ_{2}  ⇔ g_{2}
Γ ⊢ (let x_{1} ⇐ e_{1} in e_{2}) : Mτ_{2} ⇔ ⟨id_{[[Γ]]}, g_{1}⟩; t_{[[Γ]],[[τ_{1}]]}; g_{2}^{∗}

Table 1: Summary of Moggi’s Semantics • Inference Rules of Many Sorted Equational Logic:

refl {Γ ⊢ e : τ \atop Γ ⊢ e =_{τ} e}

symm {Γ ⊢ e_{2} =_{τ} e_{1} \atop Γ ⊢ e_{1} =_{τ} e_{2}}

trans \begin{matrix}Γ ⊢ e_{1} =_{τ} e_{2} & Γ ⊢ e_{2} =_{τ} e_{3} \\ Γ ⊢ e_{1} =_{τ} e_{3} \end{matrix}

congr {Γ ⊢ e_{1} =_{τ_{1}} e_{2} \atop Γ ⊢ f(e_{1}) =_{τ_{2}} f(e_{2})}

subst \begin{matrix}Γ ⊢ e : τ & Γ, x : τ ⊢ ϕ \\ Γ ⊢ [e/x]ϕ \end{matrix}

• Rules for Product Types:

1.η {Γ ⊢ e : 1 \atop Γ ⊢ ∗ =_{1} e}

⟨ ⟩.ξ \begin{matrix}Γ ⊢ e_{1} =_{τ_{1}} e_{1}′ & Γ ⊢ e_{2} =_{τ_{2}} e_{2}′ \\ Γ ⊢ ⟨e_{1}, e_{2}⟩ =_{τ_{1}×τ_{2}} ⟨e′_{1}, e′_{2}⟩ \end{matrix}

×.β \begin{matrix}Γ ⊢ e_{1} : τ_{1} & Γ ⊢ e_{2} : τ_{2} \\ Γ ⊢ π_{i}(⟨e_{1}, e_{2}⟩) =_{τ_{i}} e_{i} \end{matrix}

×.η {Γ ⊢ e : τ_{1} × τ_{2} \atop Γ ⊢ ⟨π_{1}(e), π_{2}(e)⟩ =_{τ_{1}×τ_{2}} e}

• Rules for Computational Types:

[ ].ξ {Γ ⊢ e_{1} =_{τ} e_{2} \atop Γ ⊢ [e_{1}] =_{Mτ} [e_{2}]}

let.ξ (Γ ⊢ e_{1} =_{Mτ_{1}} e_{1}′ Γ ⊢ e_{2} =_{Mτ_{2}} e_{2}′) / (Γ ⊢ (let x ⇐ e_{1} in e_{2}) =_{Mτ_{2}} (let x ⇐ e_{1}′ in e_{2}′))

ass Γ ⊢ e_{1} : Mτ_{1} Γ, x_{1} : τ_{1} ⊢ e_{2} : Mτ_{2} Γ, x_{2} : τ_{2} ⊢ e_{3} : Mτ_{3} Γ ⊢ (let x_{2} ⇐ (let x_{1} ⇐ e_{1} in e_{2}) in e_{3}) =_{Mτ_{3}} (let x_{1} ⇐ e_{1} in (let x_{2} ⇐ e_{2} in e_{3}))

M.β (Γ ⊢ e_{1} : τ_{1} Γ, x_{1} : τ_{1} ⊢ e_{2} : Mτ_{2}) / (Γ ⊢ (let x_{1} ⇐ [e_{1}] in e_{2}) =_{Mτ_{2}} [e_{1}/x_{1}]e_{2})

M.η {Γ ⊢ e_{1} : Mτ_{1} \atop Γ ⊢ (let x_{1} ⇐ [e_{1}] in [x_{1}]) =_{Mτ_{1}} e_{1}}

Table 2: Inference Rules of the Metalanguage 12

Syntax  Semantics

⊢ τ_{i} type (1 ≤ i ≤ n)

x_{1} : τ_{1}, …, x_{n} : τ_{n} ⊢ x_{i} : τ_{i}  ⇔ πi^{L}
Γ ⊢ ∗ : 1  ⇔ !_{[[Γ]]}^{L}
Γ ⊢ e_{1} : τ_{1}  ⇔ g_{1}
Γ ⊢ e_{2} : τ_{2}  ⇔ g_{2}
Γ ⊢ ⟨e_{1}, e_{2}⟩ : τ_{1} × τ_{2}  ⇔ ⟨g_{1}, g_{2}⟩^{L}
Γ ⊢ e : τ_{1} × τ_{2}  ⇔ g
Γ ⊢ π_{i}(e) : τ_{i}  ⇔ g;^{L} πi^{L}

f : τ_{1} → τ_{2} (constant)

Γ ⊢ e_{1} : τ_{1}  ⇔ g
Γ ⊢ f(e_{1}) : τ_{2}  ⇔ g;^{L} [[f]]
Γ ⊢ e : τ  ⇔ g
Γ ⊢ [e] : Mτ  ⇔ g;^{L} η_{L[[τ]]}
Γ ⊢ e_{1} : Mτ_{1}  ⇔ g_{1}
Γ, x : τ_{1} ⊢ e_{2} : Mτ_{2}  ⇔ g_{2}
Γ ⊢ (let x_{1} ⇐ e_{1} in e_{2}) : Mτ_{2} ⇔ ⟨id_{L[[Γ]]}, g_{1}⟩; t_{[[Γ]],L[[τ_{1}]]}^{L}; (m_{[[Γ]],[[τ_{1}]]}; g_{2})^{∗}

Table 3: Summary of L-strong monad Semantics of Metalanguage