Generic models for computational effects (Q860841)

The paper contains a development of a theory of Freyd-categories (a subtle generalisation of the notion of a category with finite products) and various examples of applications of Freyd-categories, including those of modelling effects in Moggi's computational lambda-calculus. The analysis of computational effects given by monads is refined here by decomposition of the construction of the Kleisli category for a monad. The setting of Freyd-categories can also be appropriately extended to account for recursion and effects that inherently contain it: partiality, non-determinism, or probablistic non-determinism. This is done through enrichment over a category which is locally countably presentable as a cartesian closed category (this includes the characteristic examples of categories \(\omega {\mathcal C}po\) and \({\mathcal P}oset\)).