Lambda the Ultimate

Copattern matching and first-class observations in OCaml, with a macro, by Paul Laforgue and Yann Regis-Gianas:

Infinite data structures are elegantly defined by means of copattern matching, a dual construction to pattern matching that expresses the outcomes of the observations of an infinite structure. We extend the OCaml programming language with copatterns, exploiting the duality between pattern matching and copattern matching. Provided that a functional programming language has GADTs, every copattern matching can be transformed into a pattern matching via a purely local syntactic transformation, a macro. The development of this extension leads us to a generalization of previous calculus of copatterns: the introduction of first-class observation queries. We study this extension both from a formal and practical point of view.

Codata isn't well supported enough in languages IMO, and supporting it via a simple macro translation will hopefully make it easier to adopt, at least for any language with GADTs.