effectful category

Last updated Apr 23, 2024

An effectful category is an identity-on-objects functor $𝕍 → ℂ$ from a monoidal category $𝕍$ (representing the pure morphisms, or “values”) to a premonoidal category $ℂ$ (representing the effectful morphisms, or “computations”), that strictly preserves all of the premonoidal structure and whose image is central.

An effectful category $𝕍 → ℂ$ is strict when both its monoidal and premonoidal categories are. A Freyd category (Levy, 2004) is an effectful category where the pure morphisms form a cartesian monoidal category.

Effectful categories assemble into the 2-category of effectful categories.

• Promonads and String Diagrams for Effectful Categories (Roman, 2022)
• Call-By-Push-Value, A Functional-Imperative Synthesis (Levy, 2004)