‘An abstract view of programming language’’ --Moggi
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:
- computations with side effects, where a program denotes a map from a store
to a pair, value and modified store.
- computations with exceptions, where a program denotes either a value or an
- partial computations, where a program denotes either a value or diverges.
- nondeterministic computations, where a program denotes a set of possible
A program is a function from values to computations.
这里我理解，program 实际上是我们已经知道了一些上下文 (context)，然后写出来的 program 描述了一个计算的过程。
譬如我们已经知道了自然数、加法，那么程序 就描述了” 把 3 加一 “这个计算过程。
First we take a category as a model for functions and develop on top a general understanding of values and computations. More precisely we introduce a unary operation on the objects of , which map an object (viewed as the set of values of type ) to an object corresponding to the set of computations of type .
这里我理解，"computations of type " 意思是，在 perform 这个 computation 后，会返回一个 value of type 。
Then a program from to , i.e. which takes as input a value of type and after performing a certain computation will return a value of type , can be identified with a morphism from to in .
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 ，Intuitively is the inclusion of values into computations and is the extension of a function from values to computations to a function from computations to computations, which first evaluates a computation and then
applies to the resulting value.
A general theorem about monads says that they are all induced by adjunctions, namely a monad over is always of the form , where is an adjunction from to some other category .
事实上给定一个 Kleisli triple ，我们也可以找到一对 adjoint functor :