Direct Models of the Computational Lambda-calculus
Carsten Führmann · Electronic Notes in Theoretical Computer Science · 1999
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.