Duoidally enriched Freyd categories
Programming Languages
2023-03-09 v1 Logic in Computer Science
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
Keywords
Cite
@article{arxiv.2301.05162,
title = {Duoidally enriched Freyd categories},
author = {Chris Heunen and Jesse Sigal},
journal= {arXiv preprint arXiv:2301.05162},
year = {2023}
}
Comments
To appear at RAMiCS 2023