Codata in Agda

June 10th, 2008 by Nils Anders Danielsson

Last Friday I mentioned that coinductive types were recently added to Agda. Nicolas Oury almost immediately realised that this leads to a loss of subject reduction. In fact, as it turned out, Coq has had the same problem for a long time.

It was also discussed whether a constructor- or destructor-based view of codata was most appropriate. Arguments were made in favour of both; it might be a good idea to support both views.

Leave a Reply