The dual of pattern matching - copattern matching

Add to your list(s) Download to your calendar using vCal

• Anton Setzer, Swansea University
• Friday 22 November 2013, 16:00-17:00
• UG10 Learning Centre.

If you have a question about this talk, please contact Paul Levy.

Because of the importance of interactive programs, which result in potentially infinite computation traces, coalgebraic data types play an important role in computer science. Coalgebraic data types are often represented in functional programming as codata types. Implicit in the formulation of codata types is that every element of the coalgebra is introduced by a constructor.

The first result demonstrated in this talk will be to show that assuming that every element of the coalgebra is introduced by a constructor results in an undecidable equality.

In order to have a decidable equality modifications were added to the rules in Agda and Coq. This results in lack of subject reduction in the theorem prover Coq and a formulation of coalgebraic types in Agda which is severely restricted.

In our joint article with Andreas Abel, Brigitte Pientka and David Thibodeau we demonstrated how, when following the well known fact in category theory that final coalgebras are the dual of initial algebras, we obtain a formulation of final and weakly final coalgebras that is completely symmetrical to that of initial or weakly initial algebras. Introduction rules for algebras are given by the constructors, whereas elimination rules correspond to recursive pattern matching. Elimination rules for coalgebras are given by destructors, whereas introduction rules are given by recursive copattern matching. The resulting theory was shown to fulfil subject reduction, while allowing nested pattern and copattern matching and even mixing of the two. In our approach full recursion was allowed.

In our talk we will introduce this approach in detail and how to program using this approach. Then we will show how to to unfold nested (co)pattern matching, reduce it to (co)recursion operators, and, in the case that should be accepted by a termination checker, to primitive (co)recursion operators.

This talk is part of the Theoretical computer science seminar series.

This talk is included in these lists:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG10 Learning Centre
• computer sience

Note that ex-directory lists are not shown.