<p>The terminology can be a bit confusing but yes there are two languages
in for instance Moggi's "Notions of Computations as Monads" (free link
here: <a href="https://core.ac.uk/download/pdf/21173011.pdf" rel="nofollow noreferrer">https://core.ac.uk/download/pdf/21173011.pdf</a>).</p>

<p>In that paper, the languages are called <span class="math-container">$\lambda_{ml}$</span>, the
metalanguage, and <span class="math-container">$\lambda_{pl}$</span> the "programming language". I believe
<span class="math-container">$\lambda_{pl}$</span> plays the role of the computational lambda calculus but
I may be mistaken.
One confusing aspect is that both languages have an explicit type
constructor <span class="math-container">$T$</span> representing the monad, but they are used differently.</p>

<p><span class="math-container">$\lambda_{ml}$</span> is a "pure" language with a monad <span class="math-container">$T$</span>, i.e., all
manipulation of the monad is explicit in the types and the function
type <span class="math-container">$\tau_1 \to \tau_2$</span> is the type of pure functions. Observe the
bind rule (from figure 3 on page 9):</p>

<p><span class="math-container">$$\frac{x   : \tau \vdash_{ml} e_1 : T \tau_1 \quad
        x_1 : \tau_1 \vdash_{ml} e_2 : T \tau_2 }
       {x :\tau \vdash_{ml} let_T x_1 \Leftarrow e_1 in e_2 : T \tau_2}$$</span></p>

<p><span class="math-container">$e_1$</span> and <span class="math-container">$e_2$</span> are explicitly typed as terms of <span class="math-container">$T \tau_1, T\tau_2$</span>
to mark that they are effectful. Every effectful expression is really
a pure term with monadic type. This is similar to how we program with
monads in Haskell where Haskell plays the role of the metalanguage and
the monad encodes effects but really we are always manipulating "pure"
terms (I put "pure" in quotes as Haskell has its own effects of
divergence and error).</p>

<p>We can see this in the semantics of the metalanguage: a term <span class="math-container">$x:\tau
\vdash_{ml} e : \tau'$</span> denotes a morphism <span class="math-container">$[\tau] \to [\tau']$</span>, the
monad doesn't arise unless we mention it.</p>

<p>On the other hand, <span class="math-container">$\lambda_{pl}$</span> is intended to be an effectful
call-by-value programming language. As such a term <span class="math-container">$x : \tau
\vdash_{pl} e : \tau'$</span> is a <em>possibly effectful</em> term that returns
values of type <span class="math-container">$\tau'$</span>, similar to languages like SML and OCaml. That
is why in the paper the function type is written <span class="math-container">$\tau \rightharpoonup
\tau'$</span> because it is the type of effectful functions, not pure
functions.</p>

<p>Compare the bind rule here (from figure 5 on page 11):
<span class="math-container">$$\frac{x   : \tau \vdash_{pl} e_1 : \tau_1 \quad
        x_1 : \tau_1 \vdash_{pl} e_2 : \tau_2 }
       {x :\tau \vdash_{pl} let x_1 \Leftarrow e_1 in e_2 : \tau_2}$$</span></p>

<p>The monad doesn't appear explicitly, but in the semantics this uses the
Kleisli extension of <span class="math-container">$e_2$</span>.
In the semantics, we see that the terms of the programming language
are interpreted in the <em>Kleisli</em> category of the monad, so a term <span class="math-container">$x :
\tau \vdash_{pl} e : \tau'$</span> denotes a morphism <span class="math-container">$[\tau] \to T[\tau']$</span>.</p>

<p><span class="math-container">$\lambda_{pl}$</span> does include an explicit monad constructor <span class="math-container">$T$</span>, which
SML and OCaml don't have as a primitive type constructor because <span class="math-container">$T a$</span>
is equivalent to <code>unit -&gt; a</code> because <code>-&gt;</code> means effectful function.</p>

CC BY-SA 4.0
2024-12-12T13:17:15.977Z
From time to time I come back here to read this answer again.
paulotorrens
CC BY-SA 4.0
2018-10-18T15:06:07.160Z
2018-10-18T19:49:36.220Z
2018-10-18T19:49:36.220Z
Max New
<p>This is a reference confusion. Sometimes I see people use the term "Moggi's computational metalanguage" to refer to the calculus presented by Moggi, and sometimes to "Moggi's computational lambda calculus". Sometimes they use <span class="math-container">$\lambda_{ml}$</span> and sometimes <span class="math-container">$\lambda_c$</span>.</p>

<p>I've always assumed they are both the same thing, but reading the abstract from a talk by Katsumata and Moegelberg, it <a href="http://www.floc-conference.org/LOLA-program-day189.html" rel="noreferrer">says</a>:</p>

<blockquote>
  <p>we show the fullness of Moggi's monadic translation from the computational lambda calculus <span class="math-container">$\lc$</span> with sums to the computational metalanguage <span class="math-container">$\lml$</span> with sums using TT-lifting and TT-closure operator.</p>
</blockquote>

<p>Aren't these languages the same thing? Where are they introduced specifically with these names? It seems like Moggi sometimes talks about <span class="math-container">$\lambda_c$</span> model for what he calls a metalanguage, but then in other paper he talks about computational lambda calculus.</p>

<reference-request><typed-lambda-calculus><monad>
What's the difference between Moggi's computational metalanguage and Moggi's lambda calculus?
Potter
# What's the difference between Moggi's computational metalanguage and Moggi's lambda calculus?

(Asked by: username_0 on 2018-09-29)

This is a reference confusion. Sometimes I see people use the term "Moggi's computational metalanguage" to refer to the calculus presented by Moggi, and sometimes to "Moggi's computational lambda calculus". Sometimes they use $\lambda\_{ml}$ and sometimes $\lambda\_c$.

I've always assumed they are both the same thing, but reading the abstract from a talk by Katsumata and Moegelberg, it [says](http://www.floc-conference.org/LOLA-program-day189.html):

> we show the fullness of Moggi's monadic translation from the computational lambda calculus $\lc$ with sums to the computational metalanguage $\lml$ with sums using TT-lifting and TT-closure operator.

Aren't these languages the same thing? Where are they introduced specifically with these names? It seems like Moggi sometimes talks about $\lambda\_c$ model for what he calls a metalanguage, but then in other paper he talks about computational lambda calculus.

**Tags:** reference-request, typed-lambda-calculus, monad

---

## 1 answers

### Answer by username_1 on 2018-10-18. Score: 4 | Accepted answer

The terminology can be a bit confusing but yes there are two languages
in for instance Moggi's "Notions of Computations as Monads" (free link
here: <https://core.ac.uk/download/pdf/21173011.pdf>).

In that paper, the languages are called $\lambda\_{ml}$, the
metalanguage, and $\lambda\_{pl}$ the "programming language". I believe
$\lambda\_{pl}$ plays the role of the computational lambda calculus but
I may be mistaken.
One confusing aspect is that both languages have an explicit type
constructor $T$ representing the monad, but they are used differently.

$\lambda\_{ml}$ is a "pure" language with a monad $T$, i.e., all
manipulation of the monad is explicit in the types and the function
type $\tau\_1 \to \tau\_2$ is the type of pure functions. Observe the
bind rule (from figure 3 on page 9):

$$\frac{x : \tau \vdash\_{ml} e\_1 : T \tau\_1 \quad
x\_1 : \tau\_1 \vdash\_{ml} e\_2 : T \tau\_2 }
{x :\tau \vdash\_{ml} let\_T x\_1 \Leftarrow e\_1 in e\_2 : T \tau\_2}$$

$e\_1$ and $e\_2$ are explicitly typed as terms of $T \tau\_1, T\tau\_2$
to mark that they are effectful. Every effectful expression is really
a pure term with monadic type. This is similar to how we program with
monads in Haskell where Haskell plays the role of the metalanguage and
the monad encodes effects but really we are always manipulating "pure"
terms (I put "pure" in quotes as Haskell has its own effects of
divergence and error).

We can see this in the semantics of the metalanguage: a term $x:\tau
\vdash\_{ml} e : \tau'$ denotes a morphism $[\tau] \to [\tau']$, the
monad doesn't arise unless we mention it.

On the other hand, $\lambda\_{pl}$ is intended to be an effectful
call-by-value programming language. As such a term $x : \tau
\vdash\_{pl} e : \tau'$ is a *possibly effectful* term that returns
values of type $\tau'$, similar to languages like SML and OCaml. That
is why in the paper the function type is written $\tau \rightharpoonup
\tau'$ because it is the type of effectful functions, not pure
functions.

Compare the bind rule here (from figure 5 on page 11):
$$\frac{x : \tau \vdash\_{pl} e\_1 : \tau\_1 \quad
x\_1 : \tau\_1 \vdash\_{pl} e\_2 : \tau\_2 }
{x :\tau \vdash\_{pl} let x\_1 \Leftarrow e\_1 in e\_2 : \tau\_2}$$

The monad doesn't appear explicitly, but in the semantics this uses the
Kleisli extension of $e\_2$.
In the semantics, we see that the terms of the programming language
are interpreted in the *Kleisli* category of the monad, so a term $x :
\tau \vdash\_{pl} e : \tau'$ denotes a morphism $[\tau] \to T[\tau']$.

$\lambda\_{pl}$ does include an explicit monad constructor $T$, which
SML and OCaml don't have as a primitive type constructor because $T a$
is equivalent to `unit -> a` because `->` means effectful function.

> **Comments:**
> **username_2**: From time to time I come back here to read this answer again.  

---

