Freyd category

A Freyd category is one way to axiomatize models of call-by-value? programming languages. It abstracts the structure of the Kleisli category of a monad, consisting of a category that models values and another category with the same objects that models computations. Freyd categories thus provide a categorical semantics for typed programming languages with side effects such as memory access or printing. This is in the spirit of the discussion at relation between type theory and category theory,...