Direct models of the computational lambda-calculus

authors: Carsten Führmann
year: 1999
url: http://dx.doi.org/10.1016/S1571-0661(04)80078-1
publisher: Elsevier BV
abstract: We introduce direct categorical models for the computational lambda-calculus. Direct models correspond to the source level of a compiler whose target level corresponds to Moggi's monadic models. That compiler is a generalised call-by-value CPS-transform. We get our direct models by identifying the algebraic structure on the Kleisli category that arises from a monadic model. We show that direct models draw our attention to previously inconspicuous, but important, classes of programs (e.g. central, copyable, and discardable programs), and we'll analyse these classes exhaustively—at a general level, and for several specific computational effects. Moreover, we show that from each direct model K we can recover the monadic model from which K arises as the Kleisli category.