Skip to Main content Skip to Navigation
Conference papers

Copattern matching and first-class observations in OCaml, with a macro

Paul Laforgue 1 Yann Régis-Gianas 2, 3
3 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
Abstract : 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. Pro- vided 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.
Complete list of metadata

Cited literature [16 references]  Display  Hide  Download
Contributor : Yann Regis-Gianas <>
Submitted on : Friday, December 1, 2017 - 11:39:20 AM
Last modification on : Saturday, April 11, 2020 - 2:03:14 AM


Files produced by the author(s)



Paul Laforgue, Yann Régis-Gianas. Copattern matching and first-class observations in OCaml, with a macro. International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131869⟩. ⟨hal-01653261⟩



Record views


Files downloads