nLab
Freyd category

Contents

Idea

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 model values and another category with the same objects โ„‚\mathbb{C} that model computations.

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 XX is an object then so is T(X)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)T(X), if it exists, has a universal property, thus decoupling this relationship.

Definition

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

  • a category ๐•\mathbb{V} with finite products;
  • a symmetric premonoidal category โ„‚\mathbb{C}, that has the same objects as ๐•\mathbb{V};
  • an identity-on-objects functor J:๐•โ†’โ„‚J: \mathbb{V} \to \mathbb{C} preserving strict symmetric premonoidal structure, whose image lies in the centre of โ„‚\mathbb{C}.

Properties

Relation to strong monads.

If TT is a strong monad on a category ๐•\mathbb{V} with finite products, then the Kleisli category of TT forms a Freyd category and JJ has a right adjoint.

Conversely, if (๐•,โ„‚,J)(\mathbb{V},\mathbb{C},J) is a Freyd category and JJ has a right adjoint RR, then the Freyd category arises as the Kleisli category of the monad RJRJ.

Relation to Lawvere theories and PROPs

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 (FinSet opโ†’๐•‹\mathrm{FinSet}^{\mathrm{op}}\to \mathbb{T}) is an ordinary Lawvere theory, then its dual (FinSetโ†’๐•‹ op\mathrm{FinSet}\to \mathbb{T}^{\mathrm{op}}) is a Freyd category.

The Lawvere theory is commutative if and only if the premonoidal category ๐•‹ op\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 FinSet bijโ†’โ„‚\mathrm{FinSet}_{\mathrm{bij}}\to \mathbb{C} is the same thing as a PROP.

Relation to monads on presheaf categories

This relates to the situation with monads as follows. If TT is a strong monad on the presheaf category ๐•^\hat{\mathbb{V}} then the Kleisli category ๐•^โ†’(๐•^) T\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 ๐•โ†’๐•^โ†’(๐•^) T\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.

References

Freyd categories were first used in

  • John Power and Hayo Thielecke โ€œEnvironments, Continuation Semantics andย Indexed Categoriesโ€, Theoretical Aspects of Computer Software, Third International Symposium, TACS โ€˜97

and named Freyd categories in

  • John Power and Hayo Thielecke, โ€œClosed Freyd- and ฮบ\kappa-Categoriesโ€, Automata, Languages and Programming, 26th International Colloquium, ICALPโ€™99

and the longer journal version of that paper has more discussion:

  • Paul Blain Levy, John Power and Hayo Thielecke, โ€œModelling environments in call-by-value programming languagesโ€, Inf. Comput. 185(2): 182-210, 2003 preprint pdf.

The definition with monoidal actions appears in

  • Paul Blain Levy, โ€œCall-by-Push-Value. A Functional/Imperative Synthesis,โ€ Semantic Structures in Computation 2, Springer, 2004; appendix B*

The idea of extending Freyd categories to monads on presheaf categories appears in

  • John Power, โ€œGeneric models for computational effectsโ€, Theor. Comput. Sci. 364(2): 254-269 (2006)

This also contains the observation that enriched Lawvere theories are examples of Freyd categories, but the precise correspondence between the concepts is given in

  • Staton, S., 2014. Freyd categories are Enriched Lawvere Theories. Electronic Notes in Theoretical Computer Science, Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013) 303, 197โ€“206. doi:10.1016/j.entcs.2014.02.010 (free).

The connection with monads in the category of profunctors is discussed in

  • Bart Jacobs, Chris Heunen, Ichiro Hasuo, โ€œCategorical semantics for arrowsโ€. J. Funct. Program. 19(3-4): 403-438. 2009. preprint pdf

and

  • Kazuyuki Asada. โ€œArrows are strong monadsโ€. Proceedings of MSFP โ€˜10. preprint pdf


  1. Having the same objects is required or implied by having an identity-on-objects functor from ๐•\mathbb{V} to โ„‚\mathbb{C}. โ†ฉ

Revised on November 8, 2017 10:10:03 by Rod Mc Guire (108.39.130.142)