¿Cuál es la diferencia entre el metalenguaje computacional de Moggi y el cálculo lambda de Moggi?

Esta es una confusión de referencia. A veces veo que la gente usa el término "metalenguaje computacional de Moggi" para referirse al cálculo presentado por Moggi, y a veces al "cálculo lambda computacional de Moggi". A veces usan $\lambda_{ml}$ y a veces $\lambda_c$ .

Siempre he asumido que ambos son lo mismo, pero al leer el resumen de una charla de Katsumata y Moegelberg, dice :

mostramos la plenitud de la traducción monádica de Moggi desde el cálculo lambda computacional $\lc$ con sumas al metalenguaje computacional $\lml$ con sumas utilizando el operador de elevación TT y cierre TT.

¿No son estos idiomas lo mismo? ¿Dónde se introducen específicamente con estos nombres? Parece que Moggi a veces habla del modelo $\lambda_c$ para lo que él llama un metalenguaje, pero luego en otro artículo habla sobre el cálculo lambda computacional.

La terminología puede ser un poco confusa, pero sí, hay dos idiomas, por ejemplo, en "Nociones de cómputos como mónadas" de Moggi (enlace gratuito aquí: https://core.ac.uk/download/pdf/21173011.pdf ).

En ese documento, los lenguajes se denominan $\lambda_{ml}$ , el metalenguaje, y $\lambda_{pl}$ el "lenguaje de programación". Creo que $\lambda_{pl}$ desempeña el papel del cálculo lambda computacional, pero puedo estar equivocado. Un aspecto confuso es que ambos lenguajes tienen un constructor de tipo explícito $T$ representa la mónada, pero se usan de manera diferente.

$\lambda_{ml}$ es un lenguaje "puro" con una mónada$T$ , es decir, toda manipulación de la mónada es explícita en los tipos y el tipo de función$\tau_1 \to \tau_2$ es el tipo de funciones puras. Observe la regla de vinculación (de la figura 3 en la página 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$ y$e_2$ se escriben explícitamente como términos de$T \tau_1, T\tau_2$ para marcar que son efectivos. Cada expresión efectiva es realmente un término puro con tipo monádico. Esto es similar a cómo programamos con mónadas en Haskell donde Haskell desempeña el papel del metalenguaje y la mónada codifica los efectos, pero realmente siempre estamos manipulando términos "puros" (pongo "puro" entre comillas ya que Haskell tiene sus propios efectos de divergencia y error).

$x:\tau \vdash_{ml} e : \tau'$$[\tau] \to [\tau']$

$\lambda_{pl}$$x : \tau \vdash_{pl} e : \tau'$$\tau'$$\tau \rightharpoonup \tau'$

$$\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}$$

$e_2$$x : \tau \vdash_{pl} e : \tau'$$[\tau] \to T[\tau']$

$\lambda_{pl}$$T$$T a$unit -> a->