‘An abstract view of programming language’’ --Moggi

# 什么是计算？(Computation)

We consider a computation as the denotation of a program, while a more ne grained (operational approach) considers a computation as a possible execution sequence for a program.

By notion of “computation” we mean a qualitative description of the denotations of programs in a certain programming language, rather than the interpretation function itself. Examples of notions of computations are:

1. computations with side effects, where a program denotes a map from a store
   to a pair, value and modified store.
2. computations with exceptions, where a program denotes either a value or an
   exception.
3. partial computations, where a program denotes either a value or diverges.
4. nondeterministic computations, where a program denotes a set of possible
   values.

# 什么是程序？(Program)

A program is a function from values to computations.

这里我理解，program 实际上是我们已经知道了一些上下文 (context)，然后写出来的 program 描述了一个计算的过程。

譬如我们已经知道了自然数、加法，那么程序$(\lambda x.x+1)3$ 就描述了” 把 3 加一 “这个计算过程。

1. First we take a category $\mathbf{C}$ as a model for functions and develop on top a general understanding of values and computations. More precisely we introduce a unary operation $T$ on the objects of $\mathbf{C}$, which map an object $A$ (viewed as the set of values of type $\tau$) to an object $TA$ corresponding to the set of computations of type $\tau$.

   这里我理解，"computations of type $\tau$" 意思是，在 perform 这个 computation 后，会返回一个 value of type $\tau$。

2. Then a program from $A$ to $B$, i.e. which takes as input a value of type $A$ and after performing a certain computation will return a value of type $B$, can be identified with a morphism from $A$ to $TB$ in $\mathbf{C}$.

3. Finally, we identify a minimum set of requirements on values and computations so that programs are the morphisms of a suitable category.

These three steps lead to Kleisli triples for modelling notions of computation and Kleisli categories for modelling categories of programs.

In Kleisli $(T,\eta,\_^*)$，Intuitively $\eta_A$ is the inclusion of values into computations and $f^*$ is the extension of a function $f$ from values to computations to a function from computations to computations, which first evaluates a computation and then
applies $f$ to the resulting value.

A general theorem about monads says that they are all induced by adjunctions, namely a monad over $\mathbf{C}$ is always of the form $(F;G,\eta,F;\varepsilon;G)$, where $(F,G,\eta,\varepsilon)$ is an adjunction from $\mathbf{C}$ to some other category $\mathbf{D}$.

事实上给定一个 Kleisli triple $(T,\eta,\_^*)$，我们也可以找到一对 adjoint functor $\mathbf{C}\xrightarrow{F}\mathbf{C}_T\xrightarrow{G}\mathbf{C}$: