by Nils Anders Danielsson on June 10, 2008.
Tagged as: Lunches.
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.