David Thibodeau, A Core Calculus for Covering Copatterns

David Thibodeau
A Core Calculus for Covering Copatterns

Functional programming languages use inductive datatypes to represent finite objects such as lists and trees. These are created by constructors and can be analyzed and manipulated by pattern matching. Infinite data, on the other hand, are modeled by the dual concept: coinductive types. We define these infinite structures not via constructors but by observations. The dual of pattern matching, called copattern matching, allows us to synthesize such data.

In this talk, we present a core calculus exploiting this dual notion to obtain a symmetric language mixing both finite and infinite data and whose operational semantics is based on copattern matching. We also describe coverage of copatterns using a non-deterministic algorithm that emulate pattern splitting used in Agda's interactive mode.