‘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
  3. partial computations, where a program denotes either a value or diverges.
  4. nondeterministic computations, where a program denotes a set of possible

# 什么是程序?(Program)

A program is a function from values to computations.

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

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

  1. First we take a category C\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 TT on the objects of C\mathbf{C}, which map an object AA (viewed as the set of values of type τ\tau) to an object TATA corresponding to the set of computations of type τ\tau.

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

  2. Then a program from AA to BB, i.e. which takes as input a value of type AA and after performing a certain computation will return a value of type BB, can be identified with a morphism from AA to TBTB in C\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,η,_)(T,\eta,\_^*),Intuitively ηA\eta_A is the inclusion of values into computations and ff^* is the extension of a function ff from values to computations to a function from computations to computations, which first evaluates a computation and then
applies ff to the resulting value.

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

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