Controlling Copatterns: There and Back Again (Extended Version)
Abstract
Copatterns give functional programs a flexible mechanism for responding to their context, and composition can greatly enhance their expressiveness. However, that same expressive power makes it harder to precisely specify the behavior of programs. Using Danvy's functional and syntactic correspondence between different semantic artifacts, we derive a full suite of semantics for copatterns, twice. First, a calculus of monolithic copatterns is taken on a journey from small-step operational semantics to abstract machine to continuation-passing style. Then within continuation-passing style, we refactor the semantics to derive a more general calculus of compositional copatterns, and take the return journey back to derive the other semantic artifacts in reverse order.
Cite
@article{arxiv.2508.12427,
title = {Controlling Copatterns: There and Back Again (Extended Version)},
author = {Paul Downen},
journal= {arXiv preprint arXiv:2508.12427},
year = {2025}
}
Comments
To find the detailed step-by-step process, which serves as their proof of correctness, see https://github.com/pdownen/derive-copat