What's the difference between Moggi's computational metalanguage and Moggi's lambda calculus?

Question

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:

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.

Answer 1

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.