Controlling Copatterns: There and Back Again (Extended Version)

TL;DR

This paper develops a comprehensive semantic framework for copatterns in functional programming, enabling precise specification and understanding of their behavior through a journey across multiple semantic artifacts.

Contribution

It introduces a full suite of semantics for copatterns, including monolithic and compositional forms, using Danvy's correspondence to enhance understanding and expressiveness.

Findings

Derived semantics from small-step to abstract machine to CPS

Refactored semantics to obtain compositional copatterns

Reconstructed semantic artifacts in reverse order

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.