University of Birmingham > Talks@bham > Theoretical computer science seminar > The dual of pattern matching - copattern matching

The dual of pattern matching - copattern matching

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.