Sequential products in effect categories

TL;DR

This paper introduces a new categorical framework for modeling multiple arguments in effectful programming languages, generalizing existing structures like Monads and Arrows to better handle effects.

Contribution

It defines a novel product concept in effect categories, enabling more comprehensive reasoning about effectful language semantics.

Findings

Generalizes categorical product for effectful functions

Provides a framework for reasoning about multiple arguments with effects

Enhances understanding of language semantics with effects

Abstract

A new categorical framework is provided for dealing with multiple arguments in a programming language with effects, for example in a language with imperative features. Like related frameworks (Monads, Arrows, Freyd categories), we distinguish two kinds of functions. In addition, we also distinguish two kinds of equations. Then, we are able to define a kind of product, that generalizes the usual categorical product. This yields a powerful tool for deriving many results about languages with effects.