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 $\mathbb{V}$ that models values and another category with the same objects $\mathbb{C}$ 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, except that page is for non-side-effecting languages. The types of the programming language are interpreted as objects of the categories. A typed term (i.e., program expression) $\Gamma\vdash t \colon X$ is interpreted as a morphism $\Gamma \to X$ in $\mathbb{C}$. Among the terms, it is often very important to identify those that are โvaluesโ, which in particular have no side effects, and these are interpreted as morphisms in $\mathbb{V}$. Freyd categories are based around premonoidal categories, which captures the fact that reordering the execution of side effects is often subtle.
Freyd categories resolve the following complaint about using monads and Kleisli categories to model impure effects in programming languages. The Kleisli category for a monad presumes the existence of some slightly higher-order types, since if $X$ is an object then so is $T(X)$, and yet it is surely possible to understand the nature of effectful computation without also assuming the existence of certain types. Freyd categories make sense even for purely first order programming languages, and the object $T(X)$, if it exists, has a universal property, thus decoupling this relationship.
A Freyd category (following Levy 04) may be defined as
An alternative but equivalent definition is as follows (following Power, Thielecke):
A Freyd category is given by
These definitions arguably violate the principle of equivalence, because they use an identity-on-objects functor in the definitions. That is, if $\mathbb{V}$ is equivalent to some $\mathbb{V}'$, and $\mathbb{C}$ is equivalent to some $\mathbb{C}'$, while $J: \mathbb{V} \to \mathbb{C}$ is a Freyd category, there may be no way to make a Freyd category $\mathbb{V}' \to \mathbb{C}'$. A resolution of this is to regard a Freyd category as a single structure, with one set of objects, two sets of morphisms, and so on; see identity-on-objects functor and M-category for further discussion.
If $T$ is a strong monad on a category $\mathbb{V}$ with finite products, then the Kleisli category of $T$ forms a Freyd category and $J$ has a right adjoint.
Conversely, if $(\mathbb{V},\mathbb{C},J)$ is a Freyd category and $J$ has a right adjoint $R$, then the Freyd category arises as the Kleisli category of the monad $RJ$.
In more detail, the passage from a strong monad to a Freyd category is as follows. If $T$ is a strong monad on a category $\mathbb{V}$ with finite products, then the Kleisli category $\mathbb{C}$ has a premonoidal structure given by $X\otimes Y=X\times Y$ on objects and where for a morphism $f:Y\to Z$ in $\mathbb{C}$ (i.e. $f:Y\to T(Z)$ in $\mathbb{V}$) then the right tensor $(X\rtimes f):X\otimes Y\to X\otimes Z$ is given by the composite $X\times Y\xrightarrow f X\times T(Z) \xrightarrow {\mathrm{str}} T(X\times Z)$ in $\mathbb{V}$. The left tensor $(f\ltimes X):Y\otimes X\to Z\otimes X$ is given by the composite $Y\times X\xrightarrow f T(Z)\times X \xrightarrow {\mathrm{str}} T(Z\times X)$ in $\mathbb{V}$. This is a premonoidal structure, and it is monoidal if and only if the monad $T$ is a commutative monad.
To give a small Freyd category is to give an enriched Lawvere theory relative to the empty sound doctrine where the enriching category is cartesian closed.
For example, if ($\mathrm{FinSet}^{\mathrm{op}}\to \mathbb{T}$) is an ordinary Lawvere theory, then its dual ($\mathrm{FinSet}\to \mathbb{T}^{\mathrm{op}}$) is a Freyd category.
The Lawvere theory is commutative if and only if the premonoidal category $\mathbb{T}^{\mathrm{op}}$ is in fact monoidal.
A minor generalization of Freyd category allows $\mathbb{V}$ to be symmetric monoidal rather than cartesian monoidal. Then a commutative Freyd category $\mathrm{FinSet}_{\mathrm{bij}}\to \mathbb{C}$ is the same thing as a PROP.
This relates to the situation with monads as follows. If $T$ is a strong monad on the presheaf category $\hat{\mathbb{V}}$ then the Kleisli category $\hat{\mathbb{V}}\to (\hat{\mathbb{V}})^T$ is a Freyd category. But also the identity-on-objects/full-and-faithful factorization of the composite $\mathbb{V}\to \hat{\mathbb{V}}\to (\hat{\mathbb{V}})^T$ yields a Freyd category over $\mathbb{V}$.
Every Freyd category arises in this way, giving a correspondence between colimit-preserving strong monads on $\hat{\mathbb{V}}$ and Freyd categories over a category $\mathbb{V}$ with products.
On the other hand, a colimit-preserving monad on $\hat{\mathbb{V}}$ is the same thing as a monad in the category of profunctors whose carrier is $\mathbb{V}$. But this is the same thing as an identity on objects functor $\mathbb{V}\to\mathbb{C}$. And this is a Freyd category if and only if the monad is strong.
The terminology โFreyd categoryโ is not explained in the papers in which it is introduced. In private communication with John Power, he wrote, explaining the motivation for the name:
In Spring 1989, Peter spent a sabbatical at Carnegie Mellon Uni in Pittsburgh. I was at Case Western Reserve Uni in Cleveland and hired a car each week to travel to Carnegie Mellon to attend Peterโs seminars, chat with him, and attend the regular weekly seminar.
He began to introduce Axiomatic Domain Theory, the leading example being the relationship between the category of omega-cpos and strict maps between them and the category with the same objects but with partial maps. For instance, he noted that the former is cartesian closed, there is an inclusion into the latter, which has a right adjoint, and I vaguely recall he noted the symmetric monoidal structure on the latter, extending finite products.
A little earlier, Eugenio Moggi extended his thesis work on partiality by proposing monads.
So the combination of the two ideas inspired the notion of Freyd-category
Freyd categories were first used in
and named Freyd categories in
and the longer journal version of that paper has more discussion:
The definition with monoidal actions appears in
The idea of extending Freyd categories to monads on presheaf categories appears in
This also contains the observation that enriched Lawvere theories are examples of Freyd categories, but the precise correspondence between the concepts is given in
The connection with monads in the bicategory of profunctors (a.k.a. arrows) is discussed in
and
Having the same objects is required or implied by having an identity-on-objects functor from $\mathbb{V}$ to $\mathbb{C}$. โฉ
Last revised on February 27, 2024 at 21:37:46. See the history of this page for a list of all contributions to it.