Duoidally enriched Freyd categories

TL;DR

This paper introduces a novel framework for Freyd categories enriched in duoidal categories, providing a third form of parallel composition and unifying various semantics in effectful programming.

Contribution

It extends Freyd categories by enriching them in duoidal categories, offering a unified approach to sequential and parallel compositions with multiple examples.

Findings

Unified framework for effectful semantics

Includes parameterised state monad and resource separation

Demonstrates change of enrichment cases

Abstract

Freyd categories provide a semantics for first-order effectful programming languages by capturing the two different orders of evaluation for products. We enrich Freyd categories in a duoidal category, which provides a new, third choice of parallel composition. Duoidal categories have two monoidal structures which account for the sequential and parallel compositions. The traditional setting is recovered as a full coreflective subcategory for a judicious choice of duoidal category. We give several worked examples of this uniform framework, including the parameterised state monad, basic separation semantics for resources, and interesting cases of change of enrichment