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

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. 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.

References

1. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: programming infinite structures by observations. In 42nd ACM SIGPLAN conference on Principle of Programming Languages, Vol. 48. ACM, 27--38.
2. Andreas M Abel and Brigitte Pientka. 2013. Wellfounded recursion with copatterns: A unified approach to termination and productivity. In 18th ACM SIGPLAN International Conference on Functional Programming, Vol. 48. ACM, 185--196.
3. John Conway. 1970. The game of life. Scientific American 223, 4 (1970), 4.
4. The Coq development team. 2009. The Coq proof assistant reference manual. LogiCal Project. http://coq.inria.fr/doc/
5. Conal Eliott. 2008. Sequences, streams, and segments. (2008). http://conal.net/blog/posts/sequences-streams-and-segments
6. Jacques Garrigue and Didier Rémy. 1999. Semi-explicit first-class polymorphism for ML. Information and Computation 155, 1--2 (1999), 134--169.
7. Gérard Huet. 1997. The zipper. Journal of functional programming 7, 05 (1997), 549--554.
8. Jean-Baptiste Jeannin, Dexter Kozen, and Alexandra Silva. 2017. CoCaml: Functional Programming with Regular Coinductive Types. Fundamenta Informaticae 150 (2017), 347--377.
9. Marina Lenisa, John Power, and Hiroshi Watanabe. 2000. Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. Electronic Notes in Theoretical Computer Science 33 (2000), 230--260.
10. Xavier Leroy, Damien Doligez, Alain Frisch, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. 2014. The OCaml system release 4.02: Documentation and user's manual. (2014).
11. Daniel R Licata, Noam Zeilberger, and Robert Harper. 2008. Focusing on binding and computation. In Logic in Computer Science, 2008. LICS'08. 23rd Annual IEEE Symposium on. IEEE, 241--252.
12. Ulf Norell. 2009. Dependently Typed Programming in Agda. In 4th International Workshop on Types in Language Design and Implementation (TLDI '09). ACM, New York, NY, USA, 1--2.
13. Dan Piponi. 2006. Evaluating cellular automata is comonadic. Blog post (2006). http://blog.sigfpe.com/2006/12/evaluating-cellular-automata-is.html
14. Anton Setzer, Andreas Abel, Brigitte Pientka, and David Thibodeau. 2014. Unnesting of copatterns. In International Conference on Rewriting Techniques and Applications. Springer, 31--45.
15. David Thibodeau, Andrew Cave, and Brigitte Pientka. 2016. Indexed codata types. In 21st ACM SIGPLAN International Conference on Functional Programming. ACM, 351--363.
16. Hongwei Xi, Chiyan Chen, and Gang Chen. 2003. Guarded recursive datatype constructors. In 32nd ACM SIGPLAN conference on Principle of Programming Languages, Vol. 38. ACM, 224--235.
17. Noam Zeilberger. 2008. Focusing and higher-order abstract syntax. In 35th ACM SIGPLAN conference on Principle of Programming Languages, Vol. 43. ACM, 359--369.