Computational Comonads and Intensional Semantics

A denotational semantics typically associates to each type a set of values and to each program a value . Intuitively, the meaning of a program is just the thing that it computes. This is a very coarse notion of meaning, since it cannot distinguish between programs that arrive at the same result through different means. Put another way, it is a very extensional notion of meaning. In order to denote the how of computation rather than just the what, we need a “more intensional” notion of meaning.

Let us consider the more general case of a categorical semantics; i.e., suppose that we have a category whose objects represent sets of semantic values.

• For each object in , we would like to be able to pick out an object representing computations that produce -values. Naturally, should be an endofunctor on .
• We should be able to run an -computation to produce an -value. This is to say that there should be an arrow .
• We should be able to

This use of morphisms from to to model algorithms from A to B fits well with an intuitive operational semantics based on the coroutine mechanism. A program responds to requests for output by performing some computation on its input (typically, to evaluate some portion of the input) until it has enough information to determine what output value to produce. Execution is lazy, in that computation is demand-driven. The operational behavior of algorithm composition can be described as follows. Let and . Then a responds to a request for output (in ) by performing an input computation over , transforming this into a computation over by applying to the prefixes of , and supplying as argument to .