computational comonad

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. (Of course, the most purely intensional notion of meaning is the trivial one that says that the meaning of a program is just the program itself, but this )

A computational comonad on a category is a quadruple , where is a comonad on and is a natural transformation satisfying the following equations:

• .

As commutative diagrams:

class Comonad w => Computational w where
  unit :: a -> w a
  -- extract . unit = id
  -- duplicate . unit = unit . unit