Unnesting of Copatterns

ABSTRACT. Inductive data such as finite lists and trees can elegantly be defined by constructors which allow programmers to analyze and manipulate finite data via pattern matching. Dually, coinductive data such as streams can be defined by observations such as head and tail and programmers can synthesize infinite data via copattern matching. This leads to a symmetric language where finite and infinite data can be nested. In this paper, we compile nested pattern and copattern matching into a core language which only supports simple non-nested (co)pattern matching. This core language may serve as an intermediate language of a compiler. We show that this translation is conservative, i.e., the multi-step reduction relation in both languages coincides for terms of the original language. Furthermore, we show that the translation preserves strong normalisation: a term of the original language is strongly normalising in one language if and only if it is so in the other.